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

Theorem eqeq12 2812
 Description: Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
eqeq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2802 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqeq2 2810 . 2 (𝐶 = 𝐷 → (𝐵 = 𝐶𝐵 = 𝐷))
31, 2sylan9bb 513 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791 This theorem is referenced by:  eqeq12d  2814  eqeqan12dALT  2816  funopg  6358  eqfnfv  6779  2f1fvneq  6996  riotaeqimp  7119  soxp  7806  tfr3  8018  xpdom2  8595  dfac5lem4  9537  kmlem9  9569  sornom  9688  zorn2lem6  9912  elwina  10097  elina  10098  bcn1  13669  summo  15066  prodmo  15282  vdwlem12  16318  pslem  17808  gaorb  18429  gsumval3eu  19017  ringinvnz1ne0  19338  cygznlem3  20261  mat1ov  21053  dmatmulcl  21105  scmatscmiddistr  21113  scmatscm  21118  1mavmul  21153  chmatval  21434  dscmet  23179  dscopn  23180  iundisj2  24153  wlkres  27460  wlkp1lem8  27470  1wlkdlem4  27925  frgr2wwlk1  28114  iundisj2f  30353  iundisj2fi  30546  pfxwlk  32483  erdszelem9  32559  satfv0  32718  satfv0fun  32731  satffunlem  32761  satffunlem1lem1  32762  satffunlem2lem1  32764  fununiq  33125  sltval2  33276  bj-opelidb  34567  bj-ideqgALT  34573  bj-idreseq  34577  bj-idreseqb  34578  bj-ideqg1  34579  bj-ideqg1ALT  34580  unirep  35151  eqeqan2d  35663  csbfv12gALTVD  41603  imasetpreimafvbijlemf1  43919  prproropf1olem4  44021  paireqne  44026  prmdvdsfmtnof1lem2  44100  uspgrsprf1  44373
 Copyright terms: Public domain W3C validator