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

Theorem eqeq12 2295
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 2289 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqeq2 2292 . 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 1623
This theorem is referenced by:  eqeq12i  2296  eqeq12d  2297  eqeqan12d  2298  funopg  5286  eqfnfv  5622  soxp  6228  tfrlem1  6391  tfrlem2  6392  tfr3  6415  th3qlem1  6764  xpdom2  6957  dfac5lem4  7753  kmlem9  7784  sornom  7903  zorn2lem6  8128  elwina  8308  elina  8309  uzindOLD  10106  bcn1  11325  summo  12190  xpnnenOLD  12488  vdwlem12  13039  pslem  14315  gaorb  14761  gsumval3eu  15190  cygznlem3  16523  dscmet  18095  dscopn  18096  iundisj2  18906  iundisj2fi  23364  iundisj2f  23366  erdszelem9  23730  fununiq  24126  sltval2  24310  nofulllem5  24360  eqfnung2  25118  grpodlcan  25376  rngoridfz  25437  eqidob  25795  unirep  26349  csbfv12gALTVD  28675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator