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  5210  xpexr  6513  bropopvvv  6648  reldmtpos  6748  zeo  10719  rpneg  11012  xrlttri  11108  difreicc  11409  cshwshashlem1  14114  gsumbagdiag  17423  psrass1lem  17424  gsumcom3fi  18275  bwthOLD  18989  cfinufil  19476  sizeusglecusg  23345  chirredi  25749  gsummpt2co  26200  truae  26611  amosym1  28224  wl-embantd  28304  itg2addnclem  28396  itg2addnclem3  28398  tz6.12-afv  30032  2wlkonot3v  30347  2spthonot3v  30348  clwlkisclwwlklem2a4  30399  frgrancvvdeqlemB  30584  lindslinindsimp2lem5  30885  bj-sngltag  32323  cdleme32e  33929
  Copyright terms: Public domain W3C validator