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

Theorem eqeqan12d 2751
Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2759. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) Shorten other proofs. (Revised by Wolf Lammen, 23-Oct-2024.)
Hypotheses
Ref Expression
eqeqan12d.1 (𝜑𝐴 = 𝐵)
eqeqan12d.2 (𝜓𝐶 = 𝐷)
Assertion
Ref Expression
eqeqan12d ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem eqeqan12d
StepHypRef Expression
1 eqeqan12d.1 . . 3 (𝜑𝐴 = 𝐵)
21eqeq1d 2739 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐶))
3 eqeqan12d.2 . . 3 (𝜓𝐶 = 𝐷)
43eqeq2d 2748 . 2 (𝜓 → (𝐵 = 𝐶𝐵 = 𝐷))
52, 4sylan9bb 511 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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729
This theorem is referenced by:  eqeqan12rd  2752  eqeq12d  2753  eqeq12  2754  eqfnfv2  6988  f1mpt  7213  soisores  7277  xpopth  7967  f1o2ndf1  8059  fnwelem  8068  fnse  8070  tz7.48lem  8392  ecopoveq  8764  xpdom2  9018  unfilem2  9262  wemaplem1  9489  suc11reg  9562  oemapval  9626  cantnf  9636  wemapwe  9640  r0weon  9955  infxpen  9957  fodomacn  9999  sornom  10220  fin1a2lem2  10344  fin1a2lem4  10346  neg11  11459  subeqrev  11584  rpnnen1lem6  12914  cnref1o  12917  xneg11  13141  injresinj  13700  modadd1  13820  modmul1  13836  modlteq  13857  sq11  14043  hashen  14254  fz1eqb  14261  eqwrd  14452  s111  14510  ccatopth  14611  wrd2ind  14618  wwlktovf1  14853  cj11  15054  sqrt11  15154  sqabs  15199  recan  15228  reeff1  16009  efieq  16052  eulerthlem2  16661  vdwlem12  16871  xpsff1o  17456  ismhm  18610  gsmsymgreq  19221  symgfixf1  19226  odf1  19351  sylow1  19392  frgpuplem  19561  isdomn  20780  cygznlem3  20992  psgnghm  21000  tgtop11  22348  fclsval  23375  vitali  24993  recosf1o  25907  dvdsmulf1o  26559  fsumvma  26577  negs11  27367  brcgr  27891  axlowdimlem15  27947  axcontlem1  27955  axcontlem4  27958  axcontlem7  27961  axcontlem8  27962  iswlk  28600  wlkswwlksf1o  28866  wwlksnextinj  28886  clwlkclwwlkf1  28996  clwwlkf1  29035  numclwwlkqhash  29361  grpoinvf  29516  hial2eq2  30091  qusker  32181  bnj554  33551  erdszelem9  33833  sategoelfvb  34053  mrsubff1  34148  msubff1  34190  mvhf1  34193  fneval  34853  topfneec2  34857  bj-imdirval3  35684  f1omptsnlem  35836  f1omptsn  35837  rdgeqoa  35870  poimirlem4  36111  poimirlem26  36133  poimirlem27  36134  ismtyval  36288  extep  36772  brdmqss  37137  wepwsolem  41398  fnwe2val  41405  aomclem8  41417  onsucf1o  41636  relexp0eq  42047  sprsymrelf1  45762  fmtnof1  45801  fmtnofac1  45836  prmdvdsfmtnof1  45853  sfprmdvdsmersenne  45869  isupwlk  46112  uspgrsprf1  46123  ismgmhm  46151  2zlidl  46306  rrx2xpref1o  46878  rrx2plord  46880  rrx2plordisom  46883  sphere  46907  line2ylem  46911
  Copyright terms: Public domain W3C validator