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

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

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