Theorem pm2.53 849

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

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

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 206  df-or 846

This theorem is referenced by:  jaoi  855  mtord  878  orel1  887  orim12dALT  910  biorfi  937  pm2.63  939  pm2.8  971  19.30  1884  19.33b  1888  r19.30  3119  r19.30OLD  3120  soxp  8066  xnn0nnn0pnf  12507  iccpnfcnv  24344  elpreq  31521  xlt2addrd  31731  xrge0iifcnv  32603  expdioph  41405  pm10.57  42773  vk15.4j  42932  vk15.4jVD  43318  sineq0ALT  43341  xrnmnfpnf  43415  disjinfi  43534  xrlexaddrp  43707  xrred  43720  xrnpnfmnf  43830  sumnnodd  43991  stoweidlem39  44400  dirkercncflem2  44465  fourierdlem101  44568  fourierswlem  44591  salexct  44695