Theorem pm2.53 850

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

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

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 847

This theorem is referenced by:  jaoi  856  mtord  878  orel1  887  orim12dALT  910  biorfriOLD  939  pm2.63  941  pm2.8  973  19.30  1880  19.33b  1884  r19.30  3126  r19.30OLD  3127  soxp  8170  xnn0nnn0pnf  12638  iccpnfcnv  24994  nnsge1  28364  elpreq  32558  xlt2addrd  32765  xrge0iifcnv  33879  expdioph  42980  pm10.57  44340  vk15.4j  44499  vk15.4jVD  44885  sineq0ALT  44908  xrnmnfpnf  44985  disjinfi  45099  xrlexaddrp  45267  xrred  45280  xrnpnfmnf  45390  sumnnodd  45551  stoweidlem39  45960  dirkercncflem2  46025  fourierdlem101  46128  fourierswlem  46151  salexct  46255