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

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

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2625 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqeq2 2632 . 2 (𝐶 = 𝐷 → (𝐵 = 𝐶𝐵 = 𝐷))
31, 2sylan9bb 735 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614
This theorem is referenced by:  eqeq12d  2636  eqeqan12dALT  2638  funopg  5890  eqfnfv  6277  2f1fvneq  6482  riotaeqimp  6599  soxp  7250  tfr3  7455  xpdom2  8015  dfac5lem4  8909  kmlem9  8940  sornom  9059  zorn2lem6  9283  elwina  9468  elina  9469  bcn1  13056  summo  14397  prodmo  14610  vdwlem12  15639  pslem  17146  gaorb  17680  gsumval3eu  18245  ringinvnz1ne0  18532  cygznlem3  19858  mat1ov  20194  dmatmulcl  20246  scmatscmiddistr  20254  scmatscm  20259  1mavmul  20294  chmatval  20574  dscmet  22317  dscopn  22318  iundisj2  23257  wlkres  26470  wlkp1lem8  26480  1wlkdlem4  26900  frgr2wwlk1  27086  iundisj2f  29289  iundisj2fi  29439  erdszelem9  30942  fununiq  31424  sltval2  31563  bj-elid  32757  unirep  33178  csbfv12gALTVD  38657  prmdvdsfmtnof1lem2  40826  uspgrsprf1  41073
  Copyright terms: Public domain W3C validator