Theorem pm2.53 371

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 368	. 2 |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
2	1	biimpi 194	1 |- ( ( ph \/ ps ) -> ( -. ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 366

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 368

This theorem is referenced by:  jaoi  377  orel1  380  pm2.63  786  pm2.8  848  19.30  1700  19.33b  1704  soxp  6812  iccpnfcnv  21529  elpreq  27542  xlt2addrd  27728  xrge0iifcnv  28069  expdioph  31131  pm10.57  31444  sumnnodd  31802  stoweidlem39  31987  dirkercncflem2  32052  fourierdlem101  32156  fourierswlem  32179  vk15.4j  33631  vk15.4jVD  34061  sineq0ALT  34084