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

Theorem eqeq12 2750
Description: Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)
Assertion
Ref Expression
eqeq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem eqeq12
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
2 id 22 . 2 (𝐶 = 𝐷𝐶 = 𝐷)
31, 2eqeqan12d 2747 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  eqeqan12dALT  2755  funopg  6539  eqfnfv  6986  2f1fvneq  7211  riotaeqimp  7344  soxp  8065  tfr3  8349  xpdom2  9017  dfac5lem4  10070  kmlem9  10102  sornom  10221  zorn2lem6  10445  elwina  10630  elina  10631  bcn1  14222  summo  15610  prodmo  15827  vdwlem12  16872  pslem  18469  gaorb  19095  gsumval3eu  19689  ringinvnz1ne0  20024  cygznlem3  20999  mat1ov  21820  dmatmulcl  21872  scmatscmiddistr  21880  scmatscm  21885  1mavmul  21920  chmatval  22201  dscmet  23951  dscopn  23952  iundisj2  24936  sltval2  27027  wlkres  28667  wlkp1lem8  28677  1wlkdlem4  29133  frgr2wwlk1  29322  iundisj2f  31561  iundisj2fi  31754  pfxwlk  33781  erdszelem9  33857  satfv0  34016  satfv0fun  34029  satffunlem  34059  satffunlem1lem1  34060  satffunlem2lem1  34062  fununiq  34406  bj-opelidb  35673  bj-ideqgALT  35679  bj-idreseq  35683  bj-idreseqb  35684  bj-ideqg1  35685  bj-ideqg1ALT  35686  unirep  36222  eqeqan2d  36743  csbfv12gALTVD  43273  fcoresf1  45393  imasetpreimafvbijlemf1  45686  prproropf1olem4  45788  paireqne  45793  prmdvdsfmtnof1lem2  45867  uspgrsprf1  46139  mndtcbas2  47199
  Copyright terms: Public domain W3C validator