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

Step	Hyp	Ref	Expression
1		df-or 372	. 2 |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
2	1	biimpi 198	1 |- ( ( ph \/ ps ) -> ( -. ph -> ps ) )

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