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

Theorem eqeqan12d 2466
Description: A useful inference for substituting definitions into an equality. (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  |-  ( ph  ->  A  =  B )
eqeqan12d.2  |-  ( ps 
->  C  =  D
)
Assertion
Ref Expression
eqeqan12d  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeqan12d
StepHypRef Expression
1 eqeqan12d.1 . . 3  |-  ( ph  ->  A  =  B )
21adantr 465 . 2  |-  ( (
ph  /\  ps )  ->  A  =  B )
3 eqeqan12d.2 . . 3  |-  ( ps 
->  C  =  D
)
43adantl 466 . 2  |-  ( (
ph  /\  ps )  ->  C  =  D )
52, 4eqeq12d 2465 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2435
This theorem is referenced by:  eqeqan12rd  2468  eqfnfv2  5967  f1mpt  6154  soisores  6208  xpopth  6824  f1o2ndf1  6893  fnwelem  6900  fnse  6902  tz7.48lem  7108  ecopoveq  7414  xpdom2  7614  unfilem2  7787  wemaplem1  7974  suc11reg  8039  oemapval  8105  cantnf  8115  cantnfOLD  8137  wemapwe  8142  wemapweOLD  8143  r0weon  8393  infxpen  8395  fodomacn  8440  sornom  8660  fin1a2lem2  8784  fin1a2lem4  8786  neg11  9875  subeqrev  9989  rpnnen1  11224  cnref1o  11226  xneg11  11425  injresinj  11908  modadd1  12015  modmul1  12022  sq11  12222  hashen  12402  fz1eqb  12408  eqwrd  12564  s111  12605  wrd2ind  12685  wwlktovf1  12877  cj11  12977  sqrt11  13078  sqabs  13122  recan  13151  reeff1  13837  efieq  13880  xpnnenOLD  13925  eulerthlem2  14294  vdwlem12  14492  xpsff1o  14947  ismhm  15947  gsmsymgreq  16436  symgfixf1  16441  odf1  16563  sylow1  16602  frgpuplem  16769  isdomn  17922  cygznlem3  18586  psgnghm  18594  tgtop11  19462  fclsval  20487  vitali  22000  recosf1o  22900  dvdsmulf1o  23448  fsumvma  23466  brcgr  24181  axlowdimlem15  24237  axcontlem1  24245  axcontlem4  24248  axcontlem7  24251  axcontlem8  24252  iswlk  24498  istrl  24517  wlknwwlkninj  24689  wlkiswwlkinj  24696  wwlkextinj  24708  clwwlkf1  24774  numclwlk1lem2f1  25072  grpoinvf  25220  hial2eq2  26002  erdszelem9  28621  mrsubff1  28852  msubff1  28894  mvhf1  28897  nodenselem5  29421  fneval  30146  topfneec2  30150  ismtyval  30272  wepwsolem  30963  fnwe2val  30971  aomclem8  30983  ismgmhm  32425  2zlidl  32567  bnj554  33825
  Copyright terms: Public domain W3C validator