Theorem pm2.53 850

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

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

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 206  df-or 847

This theorem is referenced by:  jaoi  856  mtord  879  orel1  888  orim12dALT  911  biorfi  938  pm2.63  940  pm2.8  972  19.30  1885  19.33b  1889  r19.30  3121  r19.30OLD  3122  soxp  8115  xnn0nnn0pnf  12557  iccpnfcnv  24460  elpreq  31798  xlt2addrd  32002  xrge0iifcnv  32944  expdioph  41810  pm10.57  43178  vk15.4j  43337  vk15.4jVD  43723  sineq0ALT  43746  xrnmnfpnf  43820  disjinfi  43939  xrlexaddrp  44110  xrred  44123  xrnpnfmnf  44233  sumnnodd  44394  stoweidlem39  44803  dirkercncflem2  44868  fourierdlem101  44971  fourierswlem  44994  salexct  45098