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  3103  soxp  8071  xnn0nnn0pnf  12487  iccpnfcnv  24898  nnsge1  28339  elpreq  32603  xlt2addrd  32839  xrge0iifcnv  34090  expdioph  43265  pm10.57  44612  vk15.4j  44769  vk15.4jVD  45154  sineq0ALT  45177  xrnmnfpnf  45328  disjinfi  45436  xrlexaddrp  45597  xrred  45609  xrnpnfmnf  45718  sumnnodd  45876  stoweidlem39  46283  dirkercncflem2  46348  fourierdlem101  46451  fourierswlem  46474  salexct  46578