Theorem pm2.53 851

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

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

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 848

This theorem is referenced by:  jaoi  857  mtord  879  orel1  888  orim12dALT  911  biorfriOLD  940  pm2.63  942  pm2.8  974  19.30  1882  19.33b  1886  r19.30  3099  soxp  8054  xnn0nnn0pnf  12462  iccpnfcnv  24864  nnsge1  28266  elpreq  32500  xlt2addrd  32734  xrge0iifcnv  33938  expdioph  43056  pm10.57  44404  vk15.4j  44561  vk15.4jVD  44946  sineq0ALT  44969  xrnmnfpnf  45120  disjinfi  45229  xrlexaddrp  45391  xrred  45403  xrnpnfmnf  45512  sumnnodd  45670  stoweidlem39  46077  dirkercncflem2  46142  fourierdlem101  46245  fourierswlem  46268  salexct  46372