Theorem pm2.53 865

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  jaoi  871  mtord  893  orel1  902  orim12dALT  925  pm2.63  955  pm2.8  988  19.30  1914  19.33b  1918  r19.30  3130  soxp  8139  xnn0nnn0pnf  12685  iccpnfcnv  25258  nnsge1  28722  elpreq  33117  xlt2addrd  33344  xrge0iifcnv  34558  expdioph  44009  pm10.57  45340  vk15.4j  45496  vk15.4jVD  45881  sineq0ALT  45904  xrnmnfpnf  46069  disjinfi  46176  xrlexaddrp  46333  xrred  46345  xrnpnfmnf  46453  stoweidlem39  47018  dirkercncflem2  47083  fourierdlem101  47186  fourierswlem  47209  salexct  47313