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  5370  xpexr  6721  bropopvvv  6861  reldmtpos  6961  zeo  10949  rpneg  11253  xrlttri  11349  difreicc  11656  cshwshashlem1  14452  gsumbagdiag  17896  psrass1lem  17897  gsumcom3fi  18769  bwthOLD  19777  cfinufil  20295  sizeusglecusg  24351  clwlkisclwwlklem2a4  24649  2wlkonot3v  24740  2spthonot3v  24741  frgrancvvdeqlemB  24903  chirredi  27178  gsummpt2co  27637  truae  28081  amosym1  29859  wl-embantd  29944  itg2addnclem  30034  itg2addnclem3  30036  tz6.12-afv  32092  lindslinindsimp2lem5  32773  bj-sngltag  34253  cdleme32e  35873
  Copyright terms: Public domain W3C validator