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

Theorem eqeq12 2453
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 2447 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqeq2 2450 . 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 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2434
This theorem is referenced by:  eqeq12i  2454  eqeq12d  2455  eqeqan12d  2456  funopg  5448  eqfnfv  5795  soxp  6683  tfr3  6856  th3qlem1  7204  xpdom2  7404  dfac5lem4  8294  kmlem9  8325  sornom  8444  zorn2lem6  8668  elwina  8851  elina  8852  uzindOLD  10734  bcn1  12087  summo  13192  xpnnenOLD  13490  vdwlem12  14051  pslem  15374  gaorb  15823  gsumval3eu  16379  cygznlem3  18000  mat1ov  18333  1mavmul  18357  dscmet  20163  dscopn  20164  iundisj2  21028  constr3trllem2  23535  rngoridfz  23920  iundisj2f  25930  iundisj2fi  26079  erdszelem9  27085  prodmo  27447  fununiq  27579  sltval2  27795  nofulllem5  27845  unirep  28603  2f1fvneq  30140  usgra2wlkspthlem2  30294  frg2wot1  30647  frg2woteqm  30649  dmatmulcl  30876  scmatmulcl  30883  csbfv12gALTVD  31632  bj-elid  32518
  Copyright terms: Public domain W3C validator