Theorem pm2.53 864

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

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

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 861

This theorem is referenced by:  jaoi  870  mtord  892  orel1  901  orim12dALT  924  biorfriOLD  953  pm2.63  955  pm2.8  988  19.30  1911  19.33b  1915  r19.30  3132  soxp  8126  xnn0nnn0pnf  12591  iccpnfcnv  25084  nnsge1  28517  elpreq  32855  xlt2addrd  33085  xrge0iifcnv  34304  expdioph  43733  pm10.57  45064  vk15.4j  45220  vk15.4jVD  45605  sineq0ALT  45628  xrnmnfpnf  45786  disjinfi  45893  xrlexaddrp  46051  xrred  46063  xrnpnfmnf  46171  sumnnodd  46329  stoweidlem39  46736  dirkercncflem2  46801  fourierdlem101  46904  fourierswlem  46927  salexct  47031