Theorem pm2.53 387

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

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

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 196  df-or 384

This theorem is referenced by:  jaoi  393  orel1  396  pm2.63  825  pm2.8  891  19.30  1798  19.33b  1802  soxp  7177  xnn0nnn0pnf  11253  iccpnfcnv  22551  elpreq  28744  xlt2addrd  28913  xrge0iifcnv  29307  expdioph  36608  pm10.57  37592  vk15.4j  37755  vk15.4jVD  38172  sineq0ALT  38195  xrnmnfpnf  38282  disjinfi  38375  xrlexaddrp  38509  xrred  38522  sumnnodd  38697  stoweidlem39  38932  dirkercncflem2  38997  fourierdlem101  39100  fourierswlem  39123  salexct  39228