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  5316  xpexr  6621  bropopvvv  6756  reldmtpos  6856  zeo  10831  rpneg  11124  xrlttri  11220  difreicc  11527  cshwshashlem1  14233  gsumbagdiag  17561  psrass1lem  17562  gsumcom3fi  18418  bwthOLD  19139  cfinufil  19626  sizeusglecusg  23539  chirredi  25943  gsummpt2co  26387  truae  26796  amosym1  28409  wl-embantd  28494  itg2addnclem  28584  itg2addnclem3  28586  tz6.12-afv  30220  2wlkonot3v  30535  2spthonot3v  30536  clwlkisclwwlklem2a4  30587  frgrancvvdeqlemB  30772  lindslinindsimp2lem5  31106  bj-sngltag  32779  cdleme32e  34398
  Copyright terms: Public domain W3C validator