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

Theorem eqeqan12d 2781
Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2782. (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 472 . 2 ((𝜑𝜓) → 𝐴 = 𝐵)
3 eqeqan12d.2 . . 3 (𝜓𝐶 = 𝐷)
43adantl 473 . 2 ((𝜑𝜓) → 𝐶 = 𝐷)
52, 4eqeq12d 2780 1 ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758
This theorem is referenced by:  eqeqan12rd  2783  eqfnfv2  6506  f1mpt  6714  soisores  6773  xpopth  7411  f1o2ndf1  7491  fnwelem  7498  fnse  7500  tz7.48lem  7744  ecopoveq  8056  xpdom2  8266  unfilem2  8436  wemaplem1  8662  suc11reg  8735  oemapval  8799  cantnf  8809  wemapwe  8813  r0weon  9090  infxpen  9092  fodomacn  9134  sornom  9356  fin1a2lem2  9480  fin1a2lem4  9482  neg11  10590  subeqrev  10711  rpnnen1lem6  12025  cnref1o  12028  xneg11  12253  injresinj  12802  modadd1  12920  modmul1  12936  modlteq  12957  sq11  13148  hashen  13344  fz1eqb  13352  eqwrd  13534  s111  13592  wrd2ind  13736  wrd2indOLD  13737  wwlktovf1  14001  cj11  14201  sqrt11  14302  sqabs  14346  recan  14375  reeff1  15146  efieq  15189  eulerthlem2  15780  vdwlem12  15989  xpsff1o  16508  ismhm  17617  gsmsymgreq  18129  symgfixf1  18134  odf1  18257  sylow1  18296  frgpuplem  18465  isdomn  19582  cygznlem3  20204  psgnghm  20212  tgtop11  21080  fclsval  22105  vitali  23685  recosf1o  24587  dvdsmulf1o  25225  fsumvma  25243  brcgr  26085  axlowdimlem15  26141  axcontlem1  26149  axcontlem4  26152  axcontlem7  26155  axcontlem8  26156  iswlk  26811  wlkswwlksf1o  27088  wlknwwlksninjOLD  27099  wlkwwlkinjOLD  27107  wwlksnextinj  27123  wwlksnextinjOLD  27128  clwlkclwwlkf1OLD  27259  clwlkclwwlkf1  27263  clwwlkf1OLD  27310  clwwlkf1  27315  numclwwlkqhash  27700  grpoinvf  27864  hial2eq2  28441  bnj554  31438  erdszelem9  31650  mrsubff1  31880  msubff1  31922  mvhf1  31925  fneval  32811  topfneec2  32815  f1omptsnlem  33638  f1omptsn  33639  rdgeqoa  33672  poimirlem4  33858  poimirlem26  33880  poimirlem27  33881  ismtyval  34042  extep  34501  wepwsolem  38313  fnwe2val  38320  aomclem8  38332  relexp0eq  38692  fmtnof1  42147  fmtnofac1  42182  prmdvdsfmtnof1  42199  sfprmdvdsmersenne  42220  isupwlk  42410  sprsymrelf1  42439  uspgrsprf1  42448  ismgmhm  42476  2zlidl  42627
  Copyright terms: Public domain W3C validator