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  3129  soxp  8127  xnn0nnn0pnf  12614  iccpnfcnv  25172  nnsge1  28608  elpreq  33003  xlt2addrd  33230  xrge0iifcnv  34443  expdioph  43864  pm10.57  45195  vk15.4j  45351  vk15.4jVD  45736  sineq0ALT  45759  xrnmnfpnf  45917  disjinfi  46024  xrlexaddrp  46182  xrred  46194  xrnpnfmnf  46302  sumnnodd  46460  stoweidlem39  46867  dirkercncflem2  46932  fourierdlem101  47035  fourierswlem  47058  salexct  47162