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

Theorem pm2.53 375
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 372 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
21biimpi 198 1  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  jaoi  381  orel1  384  pm2.63  797  pm2.8  861  19.30  1744  19.33b  1748  soxp  6909  iccpnfcnv  21972  elpreq  28157  xlt2addrd  28338  xrge0iifcnv  28739  expdioph  35878  pm10.57  36720  vk15.4j  36885  vk15.4jVD  37311  sineq0ALT  37334  disjinfi  37468  xrlexaddrp  37575  sumnnodd  37710  stoweidlem39  37900  dirkercncflem2  37966  fourierdlem101  38071  fourierswlem  38094  salexct  38193  xnn0nnn0pnf  39085
  Copyright terms: Public domain W3C validator