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

Theorem ineqan12d 3663
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 3656 . 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 1370    i^i cin 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3444
This theorem is referenced by:  fvun1  5872  fndmin  5920  offval  6438  ofrfval  6439  offval3  6682  fpar  6787  fisn  7789  ixxin  11429  vdwmc  14158  fvcosymgeq  16054  cssincl  18239  inmbl  21157  iundisj2  21164  itg1addlem3  21310  fh1  25174  iundisj2f  26084  iundisj2fi  26227  wfrlem4  27872
  Copyright terms: Public domain W3C validator