Theorem pm2.53 857

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

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

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 208  df-or 854

This theorem is referenced by:  jaoi  863  mtord  885  orel1  894  orim12dALT  917  biorfriOLD  946  pm2.63  948  pm2.8  980  19.30  1888  19.33b  1892  r19.30  3107  soxp  8076  xnn0nnn0pnf  12521  iccpnfcnv  24936  nnsge1  28360  elpreq  32623  xlt2addrd  32858  xrge0iifcnv  34124  expdioph  43475  pm10.57  44822  vk15.4j  44979  vk15.4jVD  45364  sineq0ALT  45387  xrnmnfpnf  45538  disjinfi  45646  xrlexaddrp  45804  xrred  45816  xrnpnfmnf  45924  sumnnodd  46082  stoweidlem39  46489  dirkercncflem2  46554  fourierdlem101  46657  fourierswlem  46680  salexct  46784