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

Theorem pm2.53 371
Description: Theorem *2.53 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm2.53  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ps ) )

Proof of Theorem pm2.53
StepHypRef Expression
1 df-or 368 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
21biimpi 194 1  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 368
This theorem is referenced by:  jaoi  377  orel1  380  pm2.63  786  pm2.8  848  19.30  1700  19.33b  1704  soxp  6812  iccpnfcnv  21529  elpreq  27542  xlt2addrd  27728  xrge0iifcnv  28069  expdioph  31131  pm10.57  31444  sumnnodd  31802  stoweidlem39  31987  dirkercncflem2  32052  fourierdlem101  32156  fourierswlem  32179  vk15.4j  33631  vk15.4jVD  34061  sineq0ALT  34084
  Copyright terms: Public domain W3C validator