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

Theorem dedth 3957
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 3964. If the inference has other hypotheses with class variable  A, these can be kept by assigning keephyp 3970 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 3912 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2428 . . 3  |-  ( ph  ->  A  =  if (
ph ,  A ,  B ) )
4 dedth.1 . . 3  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  ch )
)
53, 4syl 17 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
61, 5mpbiri 236 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   ifcif 3906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-if 3907
This theorem is referenced by:  dedth2h  3958  dedth3h  3959  orduninsuc  6675  oeoe  7299  limensuc  7746  axcc4dom  8860  inar1  9189  supsr  9525  renegcl  9926  peano5uzti  11014  uzenom  12164  seqfn  12211  seq1  12212  seqp1  12214  hashxp  12590  smadiadetr  19637  imsmet  26209  smcn  26220  nmlno0i  26321  nmblolbi  26327  blocn  26334  dipdir  26369  dipass  26372  siilem2  26379  htth  26447  normlem6  26644  normlem7tALT  26648  normsq  26663  hhssablo  26790  hhssnvt  26792  hhsssh  26796  shintcl  26859  chintcl  26861  pjhth  26922  ococ  26935  chm0  27020  chne0  27023  chocin  27024  chj0  27026  chjo  27044  h1de2ci  27085  spansn  27088  elspansn  27095  pjch1  27199  pjinormi  27216  pjige0  27220  hoaddid1  27320  hodid  27321  nmlnop0  27527  lnopunilem2  27540  elunop2  27542  lnophm  27548  nmbdoplb  27554  nmcopex  27558  nmcoplb  27559  lnopcon  27564  lnfn0  27576  lnfnmul  27577  nmbdfnlb  27579  nmcfnex  27582  nmcfnlb  27583  lnfncon  27585  riesz4  27593  riesz1  27594  cnlnadjeu  27607  pjhmop  27679  hmopidmch  27682  hmopidmpj  27683  pjss2coi  27693  pjssmi  27694  pjssge0i  27695  pjdifnormi  27696  pjidmco  27710  mdslmd1lem3  27856  mdslmd1lem4  27857  csmdsymi  27863  hatomic  27889  atord  27917  atcvat2  27918  chirred  27924  bnj941  29413  bnj944  29578  sqdivzi  30187  onsuccon  30924  onsucsuccmp  30930  limsucncmp  30932  dedths  32287  dedths2  32290
  Copyright terms: Public domain W3C validator