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

Theorem dedth 3716
Description: Weak deduction theorem that eliminates a hypothesis 
ph, making it become an antecedent. We assume that a proof exists for  ph when the class variable  A is replaced with a specific class 
B. The hypothesis  ch should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 3723. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3729 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpeuni/mmdeduction.html. (Contributed by NM, 15-May-1999.)
Hypotheses
Ref Expression
dedth.1  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  ch )
)
dedth.2  |-  ch
Assertion
Ref Expression
dedth  |-  ( ph  ->  ps )

Proof of Theorem dedth
StepHypRef Expression
1 dedth.2 . 2  |-  ch
2 iftrue 3681 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2385 . . 3  |-  ( ph  ->  A  =  if (
ph ,  A ,  B ) )
4 dedth.1 . . 3  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  ch )
)
53, 4syl 16 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
61, 5mpbiri 225 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   ifcif 3675
This theorem is referenced by:  dedth2h  3717  dedth3h  3718  orduninsuc  4756  oeoe  6771  limensuc  7213  axcc4dom  8247  inar1  8576  supsr  8913  renegcl  9289  peano5uzti  10284  uzenom  11224  seqfn  11255  seq1  11256  seqp1  11258  hashxp  11617  imsmet  22024  smcn  22035  nmlno0i  22136  nmblolbi  22142  blocn  22149  dipdir  22184  dipass  22187  siilem2  22194  htth  22262  normlem6  22458  normlem7tALT  22462  normsq  22477  hhssablo  22604  hhssnvt  22606  hhsssh  22610  shintcl  22673  chintcl  22675  pjhth  22736  ococ  22749  chm0  22834  chne0  22837  chocin  22838  chj0  22840  chjo  22858  h1de2ci  22899  spansn  22902  elspansn  22909  pjch1  23013  pjinormi  23030  pjige0  23034  hoaddid1  23135  hodid  23136  nmlnop0  23342  lnopunilem2  23355  elunop2  23357  lnophm  23363  nmbdoplb  23369  nmcopex  23373  nmcoplb  23374  lnopcon  23379  lnfn0  23391  lnfnmul  23392  nmbdfnlb  23394  nmcfnex  23397  nmcfnlb  23398  lnfncon  23400  riesz4  23408  riesz1  23409  cnlnadjeu  23422  pjhmop  23494  hmopidmch  23497  hmopidmpj  23498  pjss2coi  23508  pjssmi  23509  pjssge0i  23510  pjdifnormi  23511  pjidmco  23525  mdslmd1lem3  23671  mdslmd1lem4  23672  csmdsymi  23678  hatomic  23704  atord  23732  atcvat2  23733  chirred  23739  sqdivzi  24956  onsuccon  25895  onsucsuccmp  25901  limsucncmp  25903  bnj941  28474  bnj944  28640
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-if 3676
  Copyright terms: Public domain W3C validator