Theorem pm2.53 864

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

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

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 210  df-or 861

This theorem is referenced by:  jaoi  870  mtord  892  orel1  901  orim12dALT  924  biorfriOLD  953  pm2.63  955  pm2.8  988  19.30  1908  19.33b  1912  r19.30  3138  soxp  8121  xnn0nnn0pnf  12586  iccpnfcnv  25068  nnsge1  28498  elpreq  32811  xlt2addrd  33041  xrge0iifcnv  34264  expdioph  43635  pm10.57  44966  vk15.4j  45122  vk15.4jVD  45507  sineq0ALT  45530  xrnmnfpnf  45688  disjinfi  45795  xrlexaddrp  45953  xrred  45965  xrnpnfmnf  46073  sumnnodd  46231  stoweidlem39  46638  dirkercncflem2  46703  fourierdlem101  46806  fourierswlem  46829  salexct  46933