Theorem pm2.53 847

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 844	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2	1	biimpi 218	1 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))

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

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 209  df-or 844

This theorem is referenced by:  jaoi  853  mtord  876  orel1  885  orim12dALT  908  biorfi  935  pm2.63  937  pm2.8  969  19.30  1882  19.33b  1886  r19.30  3338  soxp  7823  xnn0nnn0pnf  11981  iccpnfcnv  23548  elpreq  30290  xlt2addrd  30482  xrge0iifcnv  31176  expdioph  39640  pm10.57  40723  vk15.4j  40882  vk15.4jVD  41268  sineq0ALT  41291  xrnmnfpnf  41367  disjinfi  41474  xrlexaddrp  41640  xrred  41653  xrnpnfmnf  41771  sumnnodd  41931  stoweidlem39  42344  dirkercncflem2  42409  fourierdlem101  42512  fourierswlem  42535  salexct  42637