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  1916  19.33b  1920  r19.30  3133  soxp  8178  xnn0nnn0pnf  12732  iccpnfcnv  25320  nnsge1  28786  elpreq  33223  xlt2addrd  33447  xrge0iifcnv  34676  expdioph  44296  pm10.57  45616  vk15.4j  45771  vk15.4jVD  46156  sineq0ALT  46179  xrnmnfpnf  46373  disjinfi  46480  xrlexaddrp  46637  xrred  46649  xrnpnfmnf  46757  stoweidlem39  47322  dirkercncflem2  47387  fourierdlem101  47490  fourierswlem  47513  salexct  47617