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

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

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2810 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqeq2 2817 . 2 (𝐶 = 𝐷 → (𝐵 = 𝐶𝐵 = 𝐷))
31, 2sylan9bb 501 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799
This theorem is referenced by:  eqeq12d  2821  eqeqan12dALT  2823  funopg  6135  eqfnfv  6533  2f1fvneq  6741  riotaeqimp  6858  soxp  7524  tfr3  7731  xpdom2  8294  dfac5lem4  9232  kmlem9  9265  sornom  9384  zorn2lem6  9608  elwina  9793  elina  9794  bcn1  13320  summo  14671  prodmo  14887  vdwlem12  15913  pslem  17411  gaorb  17941  gsumval3eu  18506  ringinvnz1ne0  18794  cygznlem3  20125  mat1ov  20465  dmatmulcl  20517  scmatscmiddistr  20525  scmatscm  20530  1mavmul  20565  chmatval  20847  dscmet  22590  dscopn  22591  iundisj2  23530  wlkres  26795  wlkp1lem8  26805  1wlkdlem4  27313  frgr2wwlk1  27504  iundisj2f  29728  iundisj2fi  29883  erdszelem9  31504  fununiq  31989  sltval2  32130  bj-elid  33401  unirep  33819  eqeqan1d  34324  eqeqan2d  34325  csbfv12gALTVD  39629  prmdvdsfmtnof1lem2  42072  uspgrsprf1  42323
  Copyright terms: Public domain W3C validator