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

Theorem pm2.53 373
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 370 . 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 368
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 370
This theorem is referenced by:  jaoi  379  orel1  382  pm2.63  786  pm2.8  846  19.30  1660  19.33b  1664  soxp  6785  iccpnfcnv  20632  elpreq  26035  xlt2addrd  26185  xrge0iifcnv  26497  expdioph  29510  pm10.57  29761  stoweidlem39  29972  vk15.4j  31533  vk15.4jVD  31950  sineq0ALT  31973
  Copyright terms: Public domain W3C validator