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

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

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2614 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqeq2 2621 . 2 (𝐶 = 𝐷 → (𝐵 = 𝐶𝐵 = 𝐷))
31, 2sylan9bb 732 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603 This theorem is referenced by:  eqeq12d  2625  eqeqan12dALT  2627  funopg  5836  eqfnfv  6219  soxp  7177  tfr3  7382  xpdom2  7940  dfac5lem4  8832  kmlem9  8863  sornom  8982  zorn2lem6  9206  elwina  9387  elina  9388  bcn1  12962  summo  14295  prodmo  14505  vdwlem12  15534  pslem  17029  gaorb  17563  gsumval3eu  18128  ringinvnz1ne0  18415  cygznlem3  19737  mat1ov  20073  dmatmulcl  20125  scmatscmiddistr  20133  scmatscm  20138  1mavmul  20173  chmatval  20453  dscmet  22187  dscopn  22188  iundisj2  23124  usgra2wlkspthlem2  26148  constr3trllem2  26179  frg2wot1  26584  frg2woteqm  26586  iundisj2f  28785  iundisj2fi  28943  erdszelem9  30435  fununiq  30913  sltval2  31053  nofulllem5  31105  bj-elid  32262  unirep  32677  csbfv12gALTVD  38157  prmdvdsfmtnof1lem2  40035  2f1fvneq  40322  riotaeqimp  40338  1wlkres  40879  1wlkp1lem8  40889  11wlkdlem4  41307  frgr2wwlk1  41494
 Copyright terms: Public domain W3C validator