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

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

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