Theorem pm2.53 852

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

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

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 849

This theorem is referenced by:  jaoi  858  mtord  880  orel1  889  orim12dALT  912  biorfriOLD  941  pm2.63  943  pm2.8  975  19.30  1881  19.33b  1885  r19.30  3120  r19.30OLD  3121  soxp  8154  xnn0nnn0pnf  12612  iccpnfcnv  24975  nnsge1  28346  elpreq  32548  xlt2addrd  32762  xrge0iifcnv  33932  expdioph  43035  pm10.57  44390  vk15.4j  44548  vk15.4jVD  44934  sineq0ALT  44957  xrnmnfpnf  45088  disjinfi  45197  xrlexaddrp  45363  xrred  45376  xrnpnfmnf  45485  sumnnodd  45645  stoweidlem39  46054  dirkercncflem2  46119  fourierdlem101  46222  fourierswlem  46245  salexct  46349