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

Theorem eqeq12 2486
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 2471 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqeq2 2482 . 2  |-  ( C  =  D  ->  ( B  =  C  <->  B  =  D ) )
31, 2sylan9bb 699 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459
This theorem is referenced by:  eqeq12iOLD  2488  eqeq12d  2489  eqeqan12dOLD  2491  funopg  5620  eqfnfv  5975  soxp  6896  tfr3  7068  xpdom2  7612  dfac5lem4  8507  kmlem9  8538  sornom  8657  zorn2lem6  8881  elwina  9064  elina  9065  uzindOLD  10955  bcn1  12359  summo  13502  xpnnenOLD  13804  vdwlem12  14369  pslem  15693  gaorb  16150  gsumval3eu  16710  cygznlem3  18403  mat1ov  18745  dmatmulcl  18797  scmatscmiddistr  18805  scmatscm  18810  1mavmul  18845  chmatval  19125  dscmet  20856  dscopn  20857  iundisj2  21722  usgra2wlkspthlem2  24324  constr3trllem2  24355  frg2wot1  24762  frg2woteqm  24764  rngoridfz  25141  iundisj2f  27150  iundisj2fi  27298  erdszelem9  28311  prodmo  28673  fununiq  28805  sltval2  29021  nofulllem5  29071  unirep  29834  2f1fvneq  31802  csbfv12gALTVD  32797  bj-elid  33690
  Copyright terms: Public domain W3C validator