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

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

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2613 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqeq2 2620 . 2 (𝐶 = 𝐷 → (𝐵 = 𝐶𝐵 = 𝐷))
31, 2sylan9bb 731 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602
This theorem is referenced by:  eqeq12d  2624  eqeqan12dALT  2626  funopg  5821  eqfnfv  6203  soxp  7154  tfr3  7359  xpdom2  7917  dfac5lem4  8809  kmlem9  8840  sornom  8959  zorn2lem6  9183  elwina  9364  elina  9365  bcn1  12919  summo  14243  prodmo  14453  vdwlem12  15482  pslem  16977  gaorb  17511  gsumval3eu  18076  ringinvnz1ne0  18363  cygznlem3  19684  mat1ov  20020  dmatmulcl  20072  scmatscmiddistr  20080  scmatscm  20085  1mavmul  20120  chmatval  20400  dscmet  22134  dscopn  22135  iundisj2  23068  usgra2wlkspthlem2  25941  constr3trllem2  25972  frg2wot1  26377  frg2woteqm  26379  iundisj2f  28578  iundisj2fi  28736  erdszelem9  30228  fununiq  30706  sltval2  30846  nofulllem5  30898  bj-elid  32045  unirep  32460  csbfv12gALTVD  37940  prmdvdsfmtnof1lem2  39819  2f1fvneq  40117  riotaeqimp  40144  1wlkres  40860  1wlkp1lem8  40870  11wlkdlem4  41288  frgr2wwlk1  41475
  Copyright terms: Public domain W3C validator