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

Theorem eqeqan12d 2453
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 2450 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2an 477 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431
This theorem is referenced by:  eqeqan12rd  2454  eqfnfv2  5793  f1mpt  5969  soisores  6013  xpopth  6610  f1o2ndf1  6675  fnwelem  6682  fnse  6684  tz7.48lem  6888  ecopoveq  7193  xpdom2  7398  unfilem2  7569  wemaplem1  7752  suc11reg  7817  oemapval  7883  cantnf  7893  cantnfOLD  7915  wemapwe  7920  wemapweOLD  7921  r0weon  8171  infxpen  8173  fodomacn  8218  sornom  8438  fin1a2lem2  8562  fin1a2lem4  8564  addsrpr  9234  mulsrpr  9235  neg11  9652  subeqrev  9763  rpnnen1  10976  cnref1o  10978  xneg11  11177  injresinj  11631  modadd1  11737  modmul1  11744  sq11  11930  hashen  12110  fz1eqb  12116  eqwrd  12257  s111  12294  wrd2ind  12364  cj11  12643  sqr11  12744  sqabs  12788  recan  12816  reeff1  13396  efieq  13439  xpnnenOLD  13484  eulerthlem2  13849  vdwlem12  14045  xpsff1o  14498  ismhm  15458  gsmsymgreq  15928  symgfixf1  15934  odf1  16054  sylow1  16093  frgpuplem  16260  isdomn  17346  cygznlem3  17982  psgnghm  17990  tgtop11  18567  fclsval  19561  vitali  21073  recosf1o  21971  dvdsmulf1o  22514  fsumvma  22532  brcgr  23114  axlowdimlem15  23170  axcontlem1  23178  axcontlem4  23181  axcontlem7  23184  axcontlem8  23185  iswlk  23394  istrl  23404  grpoinvf  23695  hial2eq2  24477  erdszelem9  27056  nodenselem5  27795  fneval  28530  topfneec2  28535  ismtyval  28670  wepwsolem  29365  fnwe2val  29373  aomclem8  29385  wwlktovf1  30223  wlknwwlkninj  30314  wlkiswwlkinj  30321  wwlkextinj  30333  clwwlkf1  30429  numclwlk1lem2f1  30658  bnj554  31821
  Copyright terms: Public domain W3C validator