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

Theorem pm2.24d 137
Description: Deduction version of pm2.24 103. (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 23 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
32con1d 118 1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.5  146  asymref2  5210  xpexr  5266  bropopvvv  6385  reldmtpos  6446  abianfp  6675  zeo  10311  rpneg  10597  xrlttri  10688  difreicc  10984  gsumbagdiag  16396  psrass1lem  16397  cfinufil  17913  sizeusglecusg  21448  chirredi  23850  truae  24547  amosym1  26080  wl-adnestantd  26123  itg2addnclem  26155  itg2addnclem3  26157  gsumcom3fi  27323  tz6.12-afv  27904  2wlkonot3v  28072  2spthonot3v  28073  frgrancvvdeqlemB  28141  cdleme32e  30927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator