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

Theorem eqeq12 2462
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 2458 . 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 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2435
This theorem is referenced by:  eqeq12iOLD  2464  eqeq12d  2465  eqeqan12dOLD  2467  funopg  5610  eqfnfv  5966  soxp  6898  tfr3  7070  xpdom2  7614  dfac5lem4  8510  kmlem9  8541  sornom  8660  zorn2lem6  8884  elwina  9067  elina  9068  uzindOLD  10964  bcn1  12373  summo  13521  prodmo  13725  xpnnenOLD  13925  vdwlem12  14492  pslem  15815  gaorb  16324  gsumval3eu  16886  cygznlem3  18586  mat1ov  18928  dmatmulcl  18980  scmatscmiddistr  18988  scmatscm  18993  1mavmul  19028  chmatval  19308  dscmet  21071  dscopn  21072  iundisj2  21937  usgra2wlkspthlem2  24598  constr3trllem2  24629  frg2wot1  25035  frg2woteqm  25037  rngoridfz  25415  iundisj2f  27427  iundisj2fi  27580  erdszelem9  28621  fununiq  29176  sltval2  29392  nofulllem5  29442  unirep  30179  2f1fvneq  32261  csbfv12gALTVD  33567  bj-elid  34474
  Copyright terms: Public domain W3C validator