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

Theorem dedth 3991
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 3998. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 4004 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 3945 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2475 . . 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 233 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940
This theorem is referenced by:  dedth2h  3992  dedth3h  3993  orduninsuc  6663  oeoe  7249  limensuc  7695  axcc4dom  8822  inar1  9154  supsr  9490  renegcl  9883  peano5uzti  10951  uzenom  12044  seqfn  12088  seq1  12089  seqp1  12091  hashxp  12459  smadiadetr  18984  imsmet  25370  smcn  25381  nmlno0i  25482  nmblolbi  25488  blocn  25495  dipdir  25530  dipass  25533  siilem2  25540  htth  25608  normlem6  25805  normlem7tALT  25809  normsq  25824  hhssablo  25952  hhssnvt  25954  hhsssh  25958  shintcl  26021  chintcl  26023  pjhth  26084  ococ  26097  chm0  26182  chne0  26185  chocin  26186  chj0  26188  chjo  26206  h1de2ci  26247  spansn  26250  elspansn  26257  pjch1  26361  pjinormi  26378  pjige0  26382  hoaddid1  26483  hodid  26484  nmlnop0  26690  lnopunilem2  26703  elunop2  26705  lnophm  26711  nmbdoplb  26717  nmcopex  26721  nmcoplb  26722  lnopcon  26727  lnfn0  26739  lnfnmul  26740  nmbdfnlb  26742  nmcfnex  26745  nmcfnlb  26746  lnfncon  26748  riesz4  26756  riesz1  26757  cnlnadjeu  26770  pjhmop  26842  hmopidmch  26845  hmopidmpj  26846  pjss2coi  26856  pjssmi  26857  pjssge0i  26858  pjdifnormi  26859  pjidmco  26873  mdslmd1lem3  27019  mdslmd1lem4  27020  csmdsymi  27026  hatomic  27052  atord  27080  atcvat2  27081  chirred  27087  sqdivzi  28855  onsuccon  29756  onsucsuccmp  29762  limsucncmp  29764  bnj941  33127  bnj944  33292  dedths  33982  dedths2  33985
  Copyright terms: Public domain W3C validator