Theorem pm2.53 848

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

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

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 210  df-or 845

This theorem is referenced by:  jaoi  854  mtord  877  orel1  886  orim12dALT  909  biorfi  936  pm2.63  938  pm2.8  970  19.30  1883  19.33b  1887  r19.30  3259  soxp  7835  xnn0nnn0pnf  12033  iccpnfcnv  23660  elpreq  30415  xlt2addrd  30619  xrge0iifcnv  31418  expdioph  40383  pm10.57  41494  vk15.4j  41653  vk15.4jVD  42039  sineq0ALT  42062  xrnmnfpnf  42138  disjinfi  42236  xrlexaddrp  42398  xrred  42411  xrnpnfmnf  42526  sumnnodd  42684  stoweidlem39  43093  dirkercncflem2  43158  fourierdlem101  43261  fourierswlem  43284  salexct  43386