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

Theorem eqeqan12d 2331
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 2328 . 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 1633
This theorem is referenced by:  eqeqan12rd  2332  eqfnfv2  5661  f1mpt  5827  soisores  5866  xpopth  6203  fnwelem  6272  fnse  6274  tz7.48lem  6495  ecopoveq  6802  xpdom2  7000  unfilem2  7167  wemaplem1  7306  suc11reg  7365  oemapval  7430  cantnf  7440  wemapwe  7445  r0weon  7685  infxpen  7687  fodomacn  7728  sornom  7948  fin1a2lem2  8072  fin1a2lem4  8074  addsrpr  8742  mulsrpr  8743  neg11  9143  rpnnen1  10394  cnref1o  10396  xneg11  10589  modadd1  11048  modmul1  11049  sq11  11223  hashen  11393  fz1eqb  11395  s111  11495  cj11  11694  sqr11  11795  sqabs  11839  recan  11867  reeff1  12447  efieq  12490  xpnnenOLD  12535  eulerthlem2  12897  vdwlem12  13086  xpsff1o  13519  ismhm  14466  odf1  14924  sylow1  14963  frgpuplem  15130  isdomn  16084  cygznlem3  16579  tgtop11  16776  fclsval  17755  vitali  19021  recosf1o  19950  dvdsmulf1o  20487  fsumvma  20505  grpoinvf  20960  hial2eq2  21741  erdszelem9  24014  subeqrev  24378  nodenselem5  24724  brcgr  24914  axlowdimlem15  24970  axcontlem1  24978  axcontlem4  24981  axcontlem7  24984  axcontlem8  24985  fneval  25436  topfneec2  25441  ismtyval  25672  wepwsolem  26286  fnwe2val  26294  aomclem8  26307  psgnghm  26585  injresinj  27277  iswlk  27439  istrl  27449  bnj554  28442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-cleq 2309
  Copyright terms: Public domain W3C validator