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

Theorem eqeqan12d 2843
Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2844. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Hypotheses
Ref Expression
eqeqan12d.1 (𝜑𝐴 = 𝐵)
eqeqan12d.2 (𝜓𝐶 = 𝐷)
Assertion
Ref Expression
eqeqan12d ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem eqeqan12d
StepHypRef Expression
1 eqeqan12d.1 . . 3 (𝜑𝐴 = 𝐵)
21adantr 481 . 2 ((𝜑𝜓) → 𝐴 = 𝐵)
3 eqeqan12d.2 . . 3 (𝜓𝐶 = 𝐷)
43adantl 482 . 2 ((𝜑𝜓) → 𝐶 = 𝐷)
52, 4eqeq12d 2842 1 ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819
This theorem is referenced by:  eqeqan12rd  2845  eqfnfv2  6801  f1mpt  7015  soisores  7074  xpopth  7726  f1o2ndf1  7814  fnwelem  7821  fnse  7823  tz7.48lem  8073  ecopoveq  8393  xpdom2  8606  unfilem2  8777  wemaplem1  9004  suc11reg  9076  oemapval  9140  cantnf  9150  wemapwe  9154  r0weon  9432  infxpen  9434  fodomacn  9476  sornom  9693  fin1a2lem2  9817  fin1a2lem4  9819  neg11  10931  subeqrev  11056  rpnnen1lem6  12376  cnref1o  12379  xneg11  12603  injresinj  13153  modadd1  13271  modmul1  13287  modlteq  13308  sq11  13491  hashen  13702  fz1eqb  13710  eqwrd  13904  s111  13964  ccatopth  14073  wrd2ind  14080  wwlktovf1  14316  cj11  14516  sqrt11  14617  sqabs  14662  recan  14691  reeff1  15468  efieq  15511  eulerthlem2  16114  vdwlem12  16323  xpsff1o  16835  ismhm  17953  gsmsymgreq  18496  symgfixf1  18501  odf1  18625  sylow1  18664  frgpuplem  18834  isdomn  20002  cygznlem3  20651  psgnghm  20659  tgtop11  21525  fclsval  22551  vitali  24148  recosf1o  25051  dvdsmulf1o  25704  fsumvma  25722  brcgr  26619  axlowdimlem15  26675  axcontlem1  26683  axcontlem4  26686  axcontlem7  26689  axcontlem8  26690  iswlk  27325  wlkswwlksf1o  27590  wwlksnextinj  27610  clwlkclwwlkf1  27721  clwwlkf1  27761  numclwwlkqhash  28087  grpoinvf  28242  hial2eq2  28817  qusker  30851  bnj554  32076  erdszelem9  32349  sategoelfvb  32569  mrsubff1  32664  msubff1  32706  mvhf1  32709  fneval  33603  topfneec2  33607  bj-imdirval3  34372  f1omptsnlem  34505  f1omptsn  34506  rdgeqoa  34539  poimirlem4  34782  poimirlem26  34804  poimirlem27  34805  ismtyval  34965  extep  35427  brdmqss  35767  wepwsolem  39526  fnwe2val  39533  aomclem8  39545  relexp0eq  39930  sprsymrelf1  43509  fmtnof1  43548  fmtnofac1  43583  prmdvdsfmtnof1  43600  sfprmdvdsmersenne  43619  isupwlk  43862  uspgrsprf1  43873  ismgmhm  43901  2zlidl  44107  rrx2xpref1o  44607  rrx2plord  44609  rrx2plordisom  44612  sphere  44636  line2ylem  44640
  Copyright terms: Public domain W3C validator