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

Theorem pm2.24d 143
Description: Deduction version of pm2.24 109. (Contributed by NM, 30-Jan-2006.)
Hypothesis
Ref Expression
pm2.24d.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
pm2.24d  |-  ( ph  ->  ( -.  ps  ->  ch ) )

Proof of Theorem pm2.24d
StepHypRef Expression
1 pm2.24d.1 . . 3  |-  ( ph  ->  ps )
21a1d 25 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
32con1d 124 1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.5  152  asymref2  5375  xpexr  6714  bropopvvv  6853  reldmtpos  6953  zeo  10935  rpneg  11238  xrlttri  11334  difreicc  11641  cshwshashlem1  14427  gsumbagdiag  17792  psrass1lem  17793  gsumcom3fi  18662  bwthOLD  19670  cfinufil  20157  sizeusglecusg  24148  clwlkisclwwlklem2a4  24446  2wlkonot3v  24537  2spthonot3v  24538  chirredi  26839  gsummpt2co  27284  truae  27705  amosym1  29318  wl-embantd  29403  itg2addnclem  29494  itg2addnclem3  29496  tz6.12-afv  31544  frgrancvvdeqlemB  31757  lindslinindsimp2lem5  32011  bj-sngltag  33497  cdleme32e  35116
  Copyright terms: Public domain W3C validator