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

Theorem dedth 3606
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 3613. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3619 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 3571 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2288 . . 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 1623   ifcif 3565
This theorem is referenced by:  dedth2h  3607  dedth3h  3608  orduninsuc  4634  oeoe  6597  limensuc  7038  axcc4dom  8067  inar1  8397  supsr  8734  renegcl  9110  peano5uzti  10101  uzenom  11027  seqfn  11058  seq1  11059  seqp1  11061  hashxp  11386  imsmet  21260  smcn  21271  nmlno0i  21372  nmblolbi  21378  blocn  21385  dipdir  21420  dipass  21423  siilem2  21430  htth  21498  normlem6  21694  normlem7tALT  21698  normsq  21713  hhssablo  21840  hhssnvt  21842  hhsssh  21846  shintcl  21909  chintcl  21911  pjhth  21972  ococ  21985  chm0  22070  chne0  22073  chocin  22074  chj0  22076  chjo  22094  h1de2ci  22135  spansn  22138  elspansn  22145  pjch1  22249  pjinormi  22266  pjige0  22270  hoaddid1  22371  hodid  22372  nmlnop0  22578  lnopunilem2  22591  elunop2  22593  lnophm  22599  nmbdoplb  22605  nmcopex  22609  nmcoplb  22610  lnopcon  22615  lnfn0  22627  lnfnmul  22628  nmbdfnlb  22630  nmcfnex  22633  nmcfnlb  22634  lnfncon  22636  riesz4  22644  riesz1  22645  cnlnadjeu  22658  pjhmop  22730  hmopidmch  22733  hmopidmpj  22734  pjss2coi  22744  pjssmi  22745  pjssge0i  22746  pjdifnormi  22747  pjidmco  22761  mdslmd1lem3  22907  mdslmd1lem4  22908  csmdsymi  22914  hatomic  22940  atord  22968  atcvat2  22969  chirred  22975  sqdivzi  24079  onsuccon  24877  onsucsuccmp  24883  limsucncmp  24885  alexeqd  24962  ac5g  25075  snelpwg  25091  hmeogrp  25537  cnegvex2b  25662  rnegvex2b  25663  ishomd  25790  bnj941  28804  bnj944  28970
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator