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

Theorem dedth 3619
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 3626. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3632 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 3584 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2301 . . 3  |-  ( ph  ->  A  =  if (
ph ,  A ,  B ) )
4 dedth.1 . . 3  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  ch )
)
53, 4syl 15 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
61, 5mpbiri 224 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   ifcif 3578
This theorem is referenced by:  dedth2h  3620  dedth3h  3621  orduninsuc  4650  oeoe  6613  limensuc  7054  axcc4dom  8083  inar1  8413  supsr  8750  renegcl  9126  peano5uzti  10117  uzenom  11043  seqfn  11074  seq1  11075  seqp1  11077  hashxp  11402  imsmet  21276  smcn  21287  nmlno0i  21388  nmblolbi  21394  blocn  21401  dipdir  21436  dipass  21439  siilem2  21446  htth  21514  normlem6  21710  normlem7tALT  21714  normsq  21729  hhssablo  21856  hhssnvt  21858  hhsssh  21862  shintcl  21925  chintcl  21927  pjhth  21988  ococ  22001  chm0  22086  chne0  22089  chocin  22090  chj0  22092  chjo  22110  h1de2ci  22151  spansn  22154  elspansn  22161  pjch1  22265  pjinormi  22282  pjige0  22286  hoaddid1  22387  hodid  22388  nmlnop0  22594  lnopunilem2  22607  elunop2  22609  lnophm  22615  nmbdoplb  22621  nmcopex  22625  nmcoplb  22626  lnopcon  22631  lnfn0  22643  lnfnmul  22644  nmbdfnlb  22646  nmcfnex  22649  nmcfnlb  22650  lnfncon  22652  riesz4  22660  riesz1  22661  cnlnadjeu  22674  pjhmop  22746  hmopidmch  22749  hmopidmpj  22750  pjss2coi  22760  pjssmi  22761  pjssge0i  22762  pjdifnormi  22763  pjidmco  22777  mdslmd1lem3  22923  mdslmd1lem4  22924  csmdsymi  22930  hatomic  22956  atord  22984  atcvat2  22985  chirred  22991  sqdivzi  24094  onsuccon  24948  onsucsuccmp  24954  limsucncmp  24956  alexeqd  25064  ac5g  25177  snelpwg  25193  hmeogrp  25639  cnegvex2b  25764  rnegvex2b  25765  ishomd  25892  bnj941  29119  bnj944  29285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator