MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineqan12d Structured version   Unicode version

Theorem ineqan12d 3695
Description: Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
Hypotheses
Ref Expression
ineq1d.1  |-  ( ph  ->  A  =  B )
ineqan12d.2  |-  ( ps 
->  C  =  D
)
Assertion
Ref Expression
ineqan12d  |-  ( (
ph  /\  ps )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )

Proof of Theorem ineqan12d
StepHypRef Expression
1 ineq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 ineqan12d.2 . 2  |-  ( ps 
->  C  =  D
)
3 ineq12 3688 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2an 477 1  |-  ( (
ph  /\  ps )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    i^i cin 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476
This theorem is referenced by:  fvun1  5929  fndmin  5979  offval  6522  ofrfval  6523  offval3  6768  fpar  6877  fisn  7876  ixxin  11535  vdwmc  14344  fvcosymgeq  16242  cssincl  18479  inmbl  21680  iundisj2  21687  itg1addlem3  21833  fh1  26198  iundisj2f  27108  iundisj2fi  27256  wfrlem4  28909
  Copyright terms: Public domain W3C validator