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

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

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2756 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqeq2 2763 . 2 (𝐶 = 𝐷 → (𝐵 = 𝐶𝐵 = 𝐷))
31, 2sylan9bb 738 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1624 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-ext 2732 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-cleq 2745 This theorem is referenced by:  eqeq12d  2767  eqeqan12dALT  2769  funopg  6075  eqfnfv  6466  2f1fvneq  6672  riotaeqimp  6789  soxp  7450  tfr3  7656  xpdom2  8212  dfac5lem4  9131  kmlem9  9164  sornom  9283  zorn2lem6  9507  elwina  9692  elina  9693  bcn1  13286  summo  14639  prodmo  14857  vdwlem12  15890  pslem  17399  gaorb  17932  gsumval3eu  18497  ringinvnz1ne0  18784  cygznlem3  20112  mat1ov  20448  dmatmulcl  20500  scmatscmiddistr  20508  scmatscm  20513  1mavmul  20548  chmatval  20828  dscmet  22570  dscopn  22571  iundisj2  23509  wlkres  26769  wlkp1lem8  26779  1wlkdlem4  27284  frgr2wwlk1  27475  iundisj2f  29702  iundisj2fi  29857  erdszelem9  31480  fununiq  31966  sltval2  32107  bj-elid  33388  unirep  33812  eqeqan1d  34321  eqeqan2d  34322  csbfv12gALTVD  39626  prmdvdsfmtnof1lem2  41999  uspgrsprf1  42257
 Copyright terms: Public domain W3C validator