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  1879  19.33b  1883  r19.30  3118  r19.30OLD  3119  soxp  8153  xnn0nnn0pnf  12610  iccpnfcnv  24989  nnsge1  28361  elpreq  32556  xlt2addrd  32769  xrge0iifcnv  33894  expdioph  43012  pm10.57  44367  vk15.4j  44526  vk15.4jVD  44912  sineq0ALT  44935  xrnmnfpnf  45023  disjinfi  45135  xrlexaddrp  45302  xrred  45315  xrnpnfmnf  45425  sumnnodd  45586  stoweidlem39  45995  dirkercncflem2  46060  fourierdlem101  46163  fourierswlem  46186  salexct  46290