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

Theorem eqeqan12d 2298
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
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 . 2  |-  ( ph  ->  A  =  B )
2 eqeqan12d.2 . 2  |-  ( ps 
->  C  =  D
)
3 eqeq12 2295 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2an 463 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623
This theorem is referenced by:  eqeqan12rd  2299  eqfnfv2  5623  f1mpt  5785  soisores  5824  xpopth  6161  fnwelem  6230  fnse  6232  tz7.48lem  6453  ecopoveq  6759  xpdom2  6957  unfilem2  7122  wemaplem1  7261  suc11reg  7320  oemapval  7385  cantnf  7395  wemapwe  7400  r0weon  7640  infxpen  7642  fodomacn  7683  sornom  7903  fin1a2lem2  8027  fin1a2lem4  8029  addsrpr  8697  mulsrpr  8698  neg11  9098  rpnnen1  10347  cnref1o  10349  xneg11  10542  modadd1  11001  modmul1  11002  sq11  11176  hashen  11346  fz1eqb  11348  s111  11448  cj11  11647  sqr11  11748  sqabs  11792  recan  11820  reeff1  12400  efieq  12443  xpnnenOLD  12488  eulerthlem2  12850  vdwlem12  13039  xpsff1o  13470  ismhm  14417  odf1  14875  sylow1  14914  frgpuplem  15081  isdomn  16035  cygznlem3  16523  tgtop11  16720  fclsval  17703  vitali  18968  recosf1o  19897  dvdsmulf1o  20434  fsumvma  20452  grpoinvf  20907  hial2eq2  21686  erdszelem9  23730  subeqrev  24092  nodenselem5  24339  brcgr  24528  axlowdimlem15  24584  axcontlem1  24592  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  isfuna  25834  fneval  26287  topfneec2  26292  ismtyval  26524  wepwsolem  27138  fnwe2val  27146  aomclem8  27159  psgnghm  27437  bnj554  28931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator