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  1881  19.33b  1885  r19.30  3101  soxp  8111  xnn0nnn0pnf  12535  iccpnfcnv  24849  nnsge1  28242  elpreq  32464  xlt2addrd  32689  xrge0iifcnv  33930  expdioph  43019  pm10.57  44367  vk15.4j  44525  vk15.4jVD  44910  sineq0ALT  44933  xrnmnfpnf  45084  disjinfi  45193  xrlexaddrp  45355  xrred  45368  xrnpnfmnf  45477  sumnnodd  45635  stoweidlem39  46044  dirkercncflem2  46109  fourierdlem101  46212  fourierswlem  46235  salexct  46339