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

Theorem eqeq12 2448
Description: Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
eqeq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2442 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqeq2 2445 . 2  |-  ( C  =  D  ->  ( B  =  C  <->  B  =  D ) )
31, 2sylan9bb 681 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652
This theorem is referenced by:  eqeq12i  2449  eqeq12d  2450  eqeqan12d  2451  funopg  5485  eqfnfv  5827  soxp  6459  tfrlem1  6636  tfrlem2  6637  tfr3  6660  th3qlem1  7010  xpdom2  7203  dfac5lem4  8007  kmlem9  8038  sornom  8157  zorn2lem6  8381  elwina  8561  elina  8562  uzindOLD  10364  bcn1  11604  summo  12511  xpnnenOLD  12809  vdwlem12  13360  pslem  14638  gaorb  15084  gsumval3eu  15513  cygznlem3  16850  dscmet  18620  dscopn  18621  iundisj2  19443  constr3trllem2  21638  rngoridfz  22023  iundisj2f  24030  iundisj2fi  24153  erdszelem9  24885  prodmo  25262  fununiq  25394  sltval2  25611  nofulllem5  25661  unirep  26414  2f1fvneq  28077  usgra2wlkspthlem2  28307  frg2wot1  28446  frg2woteqm  28448  csbfv12gALTVD  29011
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator