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

Theorem pm2.24d 137
Description: Deduction form of pm2.24 112. (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 26 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
32con1d 127 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  155  asymref2  5179  xpexr  6691  bropopvvv  6831  reldmtpos  6936  zeo  10972  rpneg  11283  xrlttri  11389  difreicc  11715  cshwshashlem1  15009  gsumbagdiag  18543  psrass1lem  18544  gsumcom3fi  19367  cfinufil  20885  sizeusglecusg  25156  clwlkisclwwlklem2a4  25454  2wlkonot3v  25545  2spthonot3v  25546  frgrancvvdeqlemB  25708  chirredi  27989  gsummpt2co  28494  truae  29018  amosym1  31035  bj-sngltag  31488  wl-embantd  31755  itg2addnclem  31900  itg2addnclem3  31902  cdleme32e  33924  tz6.12-afv  38488  sizusglecusg  39252  lindslinindsimp2lem5  39848  nn0o1gt2  39920  nnolog2flm1  39994
  Copyright terms: Public domain W3C validator