Theorem pm2.53 864

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

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

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 861

This theorem is used by:  jaoi  870  mtord  892  orel1  901  orim12dALT  924  biorfriOLD  953  pm2.63  955  pm2.8  988  19.30  1911  19.33b  1915  r19.30  3132  soxp  8121  xnn0nnn0pnf  12594  iccpnfcnv  25112  nnsge1  28545  elpreq  32883  xlt2addrd  33113  xrge0iifcnv  34332  expdioph  43778  pm10.57  45109  vk15.4j  45265  vk15.4jVD  45650  sineq0ALT  45673  xrnmnfpnf  45831  disjinfi  45938  xrlexaddrp  46096  xrred  46108  xrnpnfmnf  46216  sumnnodd  46374  stoweidlem39  46781  dirkercncflem2  46846  fourierdlem101  46949  fourierswlem  46972  salexct  47076