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

Theorem eqeq12 2308
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 2302 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqeq2 2305 . 2  |-  ( C  =  D  ->  ( B  =  C  <->  B  =  D ) )
31, 2sylan9bb 680 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632
This theorem is referenced by:  eqeq12i  2309  eqeq12d  2310  eqeqan12d  2311  funopg  5302  eqfnfv  5638  soxp  6244  tfrlem1  6407  tfrlem2  6408  tfr3  6431  th3qlem1  6780  xpdom2  6973  dfac5lem4  7769  kmlem9  7800  sornom  7919  zorn2lem6  8144  elwina  8324  elina  8325  uzindOLD  10122  bcn1  11341  summo  12206  xpnnenOLD  12504  vdwlem12  13055  pslem  14331  gaorb  14777  gsumval3eu  15206  cygznlem3  16539  dscmet  18111  dscopn  18112  iundisj2  18922  iundisj2fi  23379  iundisj2f  23381  erdszelem9  23745  prodmo  24159  fununiq  24197  sltval2  24381  nofulllem5  24431  eqfnung2  25221  grpodlcan  25479  rngoridfz  25540  eqidob  25898  unirep  26452  constr3trllem2  28397  csbfv12gALTVD  28991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator