Theorem pm2.53 852

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

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

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 849

This theorem is referenced by:  jaoi  858  mtord  880  orel1  889  orim12dALT  912  biorfriOLD  941  pm2.63  943  pm2.8  975  19.30  1883  19.33b  1887  r19.30  3105  soxp  8081  xnn0nnn0pnf  12499  iccpnfcnv  24910  nnsge1  28351  elpreq  32614  xlt2addrd  32849  xrge0iifcnv  34110  expdioph  43377  pm10.57  44724  vk15.4j  44881  vk15.4jVD  45266  sineq0ALT  45289  xrnmnfpnf  45440  disjinfi  45548  xrlexaddrp  45708  xrred  45720  xrnpnfmnf  45829  sumnnodd  45987  stoweidlem39  46394  dirkercncflem2  46459  fourierdlem101  46562  fourierswlem  46585  salexct  46689