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

Theorem dedth 3748
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 3755. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3761 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 3713 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2417 . . 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 3707
This theorem is referenced by:  dedth2h  3749  dedth3h  3750  orduninsuc  4790  oeoe  6809  limensuc  7251  axcc4dom  8285  inar1  8614  supsr  8951  renegcl  9328  peano5uzti  10323  uzenom  11267  seqfn  11298  seq1  11299  seqp1  11301  hashxp  11660  imsmet  22144  smcn  22155  nmlno0i  22256  nmblolbi  22262  blocn  22269  dipdir  22304  dipass  22307  siilem2  22314  htth  22382  normlem6  22578  normlem7tALT  22582  normsq  22597  hhssablo  22724  hhssnvt  22726  hhsssh  22730  shintcl  22793  chintcl  22795  pjhth  22856  ococ  22869  chm0  22954  chne0  22957  chocin  22958  chj0  22960  chjo  22978  h1de2ci  23019  spansn  23022  elspansn  23029  pjch1  23133  pjinormi  23150  pjige0  23154  hoaddid1  23255  hodid  23256  nmlnop0  23462  lnopunilem2  23475  elunop2  23477  lnophm  23483  nmbdoplb  23489  nmcopex  23493  nmcoplb  23494  lnopcon  23499  lnfn0  23511  lnfnmul  23512  nmbdfnlb  23514  nmcfnex  23517  nmcfnlb  23518  lnfncon  23520  riesz4  23528  riesz1  23529  cnlnadjeu  23542  pjhmop  23614  hmopidmch  23617  hmopidmpj  23618  pjss2coi  23628  pjssmi  23629  pjssge0i  23630  pjdifnormi  23631  pjidmco  23645  mdslmd1lem3  23791  mdslmd1lem4  23792  csmdsymi  23798  hatomic  23824  atord  23852  atcvat2  23853  chirred  23859  sqdivzi  25145  onsuccon  26100  onsucsuccmp  26106  limsucncmp  26108  bnj941  28861  bnj944  29027
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
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 2399  df-cleq 2405  df-clel 2408  df-if 3708
  Copyright terms: Public domain W3C validator