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  3107  soxp  8128  xnn0nnn0pnf  12587  iccpnfcnv  24893  nnsge1  28287  elpreq  32509  xlt2addrd  32736  xrge0iifcnv  33964  expdioph  43047  pm10.57  44395  vk15.4j  44553  vk15.4jVD  44938  sineq0ALT  44961  xrnmnfpnf  45107  disjinfi  45216  xrlexaddrp  45379  xrred  45392  xrnpnfmnf  45501  sumnnodd  45659  stoweidlem39  46068  dirkercncflem2  46133  fourierdlem101  46236  fourierswlem  46259  salexct  46363