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

Theorem dedth 3695
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 3702. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3708 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 3660 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2371 . . 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 1647   ifcif 3654
This theorem is referenced by:  dedth2h  3696  dedth3h  3697  orduninsuc  4737  oeoe  6739  limensuc  7181  axcc4dom  8214  inar1  8544  supsr  8881  renegcl  9257  peano5uzti  10252  uzenom  11191  seqfn  11222  seq1  11223  seqp1  11225  hashxp  11584  imsmet  21573  smcn  21584  nmlno0i  21685  nmblolbi  21691  blocn  21698  dipdir  21733  dipass  21736  siilem2  21743  htth  21811  normlem6  22007  normlem7tALT  22011  normsq  22026  hhssablo  22153  hhssnvt  22155  hhsssh  22159  shintcl  22222  chintcl  22224  pjhth  22285  ococ  22298  chm0  22383  chne0  22386  chocin  22387  chj0  22389  chjo  22407  h1de2ci  22448  spansn  22451  elspansn  22458  pjch1  22562  pjinormi  22579  pjige0  22583  hoaddid1  22684  hodid  22685  nmlnop0  22891  lnopunilem2  22904  elunop2  22906  lnophm  22912  nmbdoplb  22918  nmcopex  22922  nmcoplb  22923  lnopcon  22928  lnfn0  22940  lnfnmul  22941  nmbdfnlb  22943  nmcfnex  22946  nmcfnlb  22947  lnfncon  22949  riesz4  22957  riesz1  22958  cnlnadjeu  22971  pjhmop  23043  hmopidmch  23046  hmopidmpj  23047  pjss2coi  23057  pjssmi  23058  pjssge0i  23059  pjdifnormi  23060  pjidmco  23074  mdslmd1lem3  23220  mdslmd1lem4  23221  csmdsymi  23227  hatomic  23253  atord  23281  atcvat2  23282  chirred  23288  sqdivzi  24668  onsuccon  25619  onsucsuccmp  25625  limsucncmp  25627  bnj941  28568  bnj944  28734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-if 3655
  Copyright terms: Public domain W3C validator