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

Theorem pm2.53 374
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 371 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
21biimpi 197 1  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 369
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 188  df-or 371
This theorem is referenced by:  jaoi  380  orel1  383  pm2.63  795  pm2.8  858  19.30  1736  19.33b  1740  soxp  6916  iccpnfcnv  21958  elpreq  28145  xlt2addrd  28331  xrge0iifcnv  28734  expdioph  35797  pm10.57  36577  vk15.4j  36742  vk15.4jVD  37171  sineq0ALT  37194  disjinfi  37317  xrlexaddrp  37416  sumnnodd  37529  stoweidlem39  37719  dirkercncflem2  37785  fourierdlem101  37890  fourierswlem  37913
  Copyright terms: Public domain W3C validator