Theorem pm2.53 865

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  jaoi  871  mtord  893  orel1  902  orim12dALT  925  pm2.63  955  pm2.8  988  19.30  1914  19.33b  1918  r19.30  3134  soxp  8127  xnn0nnn0pnf  12601  iccpnfcnv  25132  nnsge1  28565  elpreq  32903  xlt2addrd  33133  xrge0iifcnv  34346  expdioph  43783  pm10.57  45114  vk15.4j  45270  vk15.4jVD  45655  sineq0ALT  45678  xrnmnfpnf  45836  disjinfi  45943  xrlexaddrp  46101  xrred  46113  xrnpnfmnf  46221  sumnnodd  46379  stoweidlem39  46786  dirkercncflem2  46851  fourierdlem101  46954  fourierswlem  46977  salexct  47081