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

Theorem ineqan12d 3688
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 3681 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2an 475 1  |-  ( (
ph  /\  ps )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468
This theorem is referenced by:  fvun1  5919  fndmin  5970  offval  6520  ofrfval  6521  offval3  6767  fpar  6877  fisn  7879  ixxin  11549  vdwmc  14580  fvcosymgeq  16653  cssincl  18892  inmbl  22118  iundisj2  22125  itg1addlem3  22271  fh1  26734  iundisj2f  27660  iundisj2fi  27836  wfrlem4  29586  offval0  33365
  Copyright terms: Public domain W3C validator