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 215	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 206  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  1884  19.33b  1888  r19.30  3268  r19.30OLD  3269  soxp  7970  xnn0nnn0pnf  12318  iccpnfcnv  24107  elpreq  30878  xlt2addrd  31081  xrge0iifcnv  31883  expdioph  40845  pm10.57  41989  vk15.4j  42148  vk15.4jVD  42534  sineq0ALT  42557  xrnmnfpnf  42633  disjinfi  42731  xrlexaddrp  42891  xrred  42904  xrnpnfmnf  43015  sumnnodd  43171  stoweidlem39  43580  dirkercncflem2  43645  fourierdlem101  43748  fourierswlem  43771  salexct  43873