Theorem pm2.53 848

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

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

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 845

This theorem is referenced by:  jaoi  854  mtord  877  orel1  886  orim12dALT  909  biorfi  936  pm2.63  938  pm2.8  970  19.30  1882  19.33b  1886  r19.30  3293  soxp  7806  xnn0nnn0pnf  11968  iccpnfcnv  23549  elpreq  30302  xlt2addrd  30508  xrge0iifcnv  31286  expdioph  39964  pm10.57  41075  vk15.4j  41234  vk15.4jVD  41620  sineq0ALT  41643  xrnmnfpnf  41719  disjinfi  41820  xrlexaddrp  41984  xrred  41997  xrnpnfmnf  42114  sumnnodd  42272  stoweidlem39  42681  dirkercncflem2  42746  fourierdlem101  42849  fourierswlem  42872  salexct  42974