Theorem pm2.53 862

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

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

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 209  df-or 859

This theorem is referenced by:  jaoi  868  mtord  890  orel1  899  orim12dALT  922  biorfriOLD  951  pm2.63  953  pm2.8  985  19.30  1900  19.33b  1904  r19.30  3128  soxp  8103  xnn0nnn0pnf  12561  iccpnfcnv  24994  nnsge1  28424  elpreq  32687  xlt2addrd  32922  xrge0iifcnv  34191  expdioph  43561  pm10.57  44908  vk15.4j  45065  vk15.4jVD  45450  sineq0ALT  45473  xrnmnfpnf  45624  disjinfi  45731  xrlexaddrp  45889  xrred  45901  xrnpnfmnf  46009  sumnnodd  46167  stoweidlem39  46574  dirkercncflem2  46639  fourierdlem101  46742  fourierswlem  46765  salexct  46869