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

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

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2825 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqeq2 2833 . 2 (𝐶 = 𝐷 → (𝐵 = 𝐶𝐵 = 𝐷))
31, 2sylan9bb 510 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  eqeq12d  2837  eqeqan12dALT  2839  funopg  6383  eqfnfv  6795  2f1fvneq  7009  riotaeqimp  7129  soxp  7814  tfr3  8026  xpdom2  8601  dfac5lem4  9541  kmlem9  9573  sornom  9688  zorn2lem6  9912  elwina  10097  elina  10098  bcn1  13663  summo  15064  prodmo  15280  vdwlem12  16318  pslem  17806  gaorb  18377  gsumval3eu  18955  ringinvnz1ne0  19273  cygznlem3  20646  mat1ov  20987  dmatmulcl  21039  scmatscmiddistr  21047  scmatscm  21052  1mavmul  21087  chmatval  21367  dscmet  23111  dscopn  23112  iundisj2  24079  wlkres  27380  wlkp1lem8  27390  1wlkdlem4  27847  frgr2wwlk1  28036  iundisj2f  30269  iundisj2fi  30447  pfxwlk  32268  erdszelem9  32344  satfv0  32503  satfv0fun  32516  satffunlem  32546  satffunlem1lem1  32547  satffunlem2lem1  32549  fununiq  32910  sltval2  33061  bj-opelidb  34337  bj-ideqgALT  34343  bj-idreseq  34347  bj-idreseqb  34348  bj-ideqg1  34349  bj-ideqg1ALT  34350  unirep  34871  eqeqan2d  35386  csbfv12gALTVD  41113  prproropf1olem4  43515  paireqne  43520  prmdvdsfmtnof1lem2  43594  uspgrsprf1  43869
  Copyright terms: Public domain W3C validator