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  5191  xpexr  5247  bropopvvv  6365  reldmtpos  6423  abianfp  6652  zeo  10287  rpneg  10573  xrlttri  10664  difreicc  10960  gsumbagdiag  16368  psrass1lem  16369  cfinufil  17881  sizeusglecusg  21361  chirredi  23745  truae  24388  amosym1  25890  wl-adnestantd  25933  itg2addnclem  25957  gsumcom3fi  27124  tz6.12-afv  27706  frgrancvvdeqlemB  27790  cdleme32e  30559
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator