Theorem pm2.53 851

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

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

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 207  df-or 848

This theorem is referenced by:  jaoi  857  mtord  879  orel1  888  orim12dALT  911  biorfriOLD  940  pm2.63  942  pm2.8  974  19.30  1881  19.33b  1885  r19.30  3100  soxp  8108  xnn0nnn0pnf  12528  iccpnfcnv  24842  nnsge1  28235  elpreq  32457  xlt2addrd  32682  xrge0iifcnv  33923  expdioph  43012  pm10.57  44360  vk15.4j  44518  vk15.4jVD  44903  sineq0ALT  44926  xrnmnfpnf  45077  disjinfi  45186  xrlexaddrp  45348  xrred  45361  xrnpnfmnf  45470  sumnnodd  45628  stoweidlem39  46037  dirkercncflem2  46102  fourierdlem101  46205  fourierswlem  46228  salexct  46332