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

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

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2775 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqeq2 2782 . 2 (𝐶 = 𝐷 → (𝐵 = 𝐶𝐵 = 𝐷))
31, 2sylan9bb 499 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764
This theorem is referenced by:  eqeq12d  2786  eqeqan12dALT  2788  funopg  6063  eqfnfv  6453  2f1fvneq  6659  riotaeqimp  6776  soxp  7441  tfr3  7648  xpdom2  8211  dfac5lem4  9149  kmlem9  9182  sornom  9301  zorn2lem6  9525  elwina  9710  elina  9711  bcn1  13300  summo  14652  prodmo  14869  vdwlem12  15899  pslem  17410  gaorb  17943  gsumval3eu  18508  ringinvnz1ne0  18796  cygznlem3  20129  mat1ov  20468  dmatmulcl  20520  scmatscmiddistr  20528  scmatscm  20533  1mavmul  20568  chmatval  20850  dscmet  22593  dscopn  22594  iundisj2  23533  wlkres  26798  wlkp1lem8  26808  1wlkdlem4  27316  frgr2wwlk1  27507  iundisj2f  29737  iundisj2fi  29892  erdszelem9  31515  fununiq  32001  sltval2  32142  bj-elid  33418  unirep  33835  eqeqan1d  34344  eqeqan2d  34345  csbfv12gALTVD  39654  prmdvdsfmtnof1lem2  42022  uspgrsprf1  42280
  Copyright terms: Public domain W3C validator