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  3104  soxp  8079  xnn0nnn0pnf  12523  iccpnfcnv  24911  nnsge1  28335  elpreq  32598  xlt2addrd  32832  xrge0iifcnv  34077  expdioph  43451  pm10.57  44798  vk15.4j  44955  vk15.4jVD  45340  sineq0ALT  45363  xrnmnfpnf  45514  disjinfi  45622  xrlexaddrp  45782  xrred  45794  xrnpnfmnf  45902  sumnnodd  46060  stoweidlem39  46467  dirkercncflem2  46532  fourierdlem101  46635  fourierswlem  46658  salexct  46762