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

Theorem eqeqan12d 2838
Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2839. (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 2837 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:  eqeqan12rd  2840  eqfnfv2  6796  f1mpt  7010  soisores  7069  xpopth  7721  f1o2ndf1  7809  fnwelem  7816  fnse  7818  tz7.48lem  8068  ecopoveq  8388  xpdom2  8601  unfilem2  8772  wemaplem1  8999  suc11reg  9071  oemapval  9135  cantnf  9145  wemapwe  9149  r0weon  9427  infxpen  9429  fodomacn  9471  sornom  9688  fin1a2lem2  9812  fin1a2lem4  9814  neg11  10926  subeqrev  11051  rpnnen1lem6  12371  cnref1o  12374  xneg11  12598  injresinj  13148  modadd1  13266  modmul1  13282  modlteq  13303  sq11  13486  hashen  13697  fz1eqb  13705  eqwrd  13899  s111  13959  ccatopth  14068  wrd2ind  14075  wwlktovf1  14311  cj11  14511  sqrt11  14612  sqabs  14657  recan  14686  reeff1  15463  efieq  15506  eulerthlem2  16109  vdwlem12  16318  xpsff1o  16830  ismhm  17948  gsmsymgreq  18491  symgfixf1  18496  odf1  18620  sylow1  18659  frgpuplem  18829  isdomn  19997  cygznlem3  20646  psgnghm  20654  tgtop11  21520  fclsval  22546  vitali  24143  recosf1o  25046  dvdsmulf1o  25699  fsumvma  25717  brcgr  26614  axlowdimlem15  26670  axcontlem1  26678  axcontlem4  26681  axcontlem7  26684  axcontlem8  26685  iswlk  27320  wlkswwlksf1o  27585  wwlksnextinj  27605  clwlkclwwlkf1  27716  clwwlkf1  27756  numclwwlkqhash  28082  grpoinvf  28237  hial2eq2  28812  qusker  30846  bnj554  32071  erdszelem9  32344  sategoelfvb  32564  mrsubff1  32659  msubff1  32701  mvhf1  32704  fneval  33598  topfneec2  33602  bj-imdirval3  34367  f1omptsnlem  34500  f1omptsn  34501  rdgeqoa  34534  poimirlem4  34778  poimirlem26  34800  poimirlem27  34801  ismtyval  34961  extep  35423  brdmqss  35763  wepwsolem  39522  fnwe2val  39529  aomclem8  39541  relexp0eq  39926  sprsymrelf1  43505  fmtnof1  43544  fmtnofac1  43579  prmdvdsfmtnof1  43596  sfprmdvdsmersenne  43615  isupwlk  43858  uspgrsprf1  43869  ismgmhm  43897  2zlidl  44103  rrx2xpref1o  44603  rrx2plord  44605  rrx2plordisom  44608  sphere  44632  line2ylem  44636
  Copyright terms: Public domain W3C validator