Theorem pm2.53 388

Description: Theorem *2.53 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm2.53	⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))

Proof of Theorem pm2.53

Step	Hyp	Ref	Expression
1		df-or 385	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2	1	biimpi 206	1 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  jaoi  394  orel1  397  pm2.63  829  pm2.8  895  19.30  1809  19.33b  1813  soxp  7290  xnn0nnn0pnf  11376  iccpnfcnv  22743  elpreq  29360  xlt2addrd  29523  xrge0iifcnv  29979  expdioph  37590  pm10.57  38570  vk15.4j  38734  vk15.4jVD  39150  sineq0ALT  39173  xrnmnfpnf  39256  disjinfi  39380  xrlexaddrp  39568  xrred  39581  xrnpnfmnf  39705  sumnnodd  39862  stoweidlem39  40256  dirkercncflem2  40321  fourierdlem101  40424  fourierswlem  40447  salexct  40552