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  1913  19.33b  1917  r19.30  3129  soxp  8144  xnn0nnn0pnf  12696  iccpnfcnv  25271  nnsge1  28735  elpreq  33172  xlt2addrd  33398  xrge0iifcnv  34612  expdioph  44124  pm10.57  45449  vk15.4j  45605  vk15.4jVD  45990  sineq0ALT  46013  xrnmnfpnf  46194  disjinfi  46301  xrlexaddrp  46458  xrred  46470  xrnpnfmnf  46578  stoweidlem39  47143  dirkercncflem2  47208  fourierdlem101  47311  fourierswlem  47334  salexct  47438