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 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  5243  xpexr  5299  bropopvvv  6418  reldmtpos  6479  abianfp  6708  zeo  10347  rpneg  10633  xrlttri  10724  difreicc  11020  gsumbagdiag  16433  psrass1lem  16434  bwth  17465  cfinufil  17952  sizeusglecusg  21487  chirredi  23889  truae  24586  amosym1  26168  wl-adnestantd  26211  itg2addnclem  26246  itg2addnclem3  26248  gsumcom3fi  27423  tz6.12-afv  28004  cshwssizelem3  28245  2wlkonot3v  28295  2spthonot3v  28296  frgrancvvdeqlemB  28364  cdleme32e  31179
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator