Theorem pm2.53 847

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

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

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 206  df-or 844

This theorem is referenced by:  jaoi  853  mtord  876  orel1  885  orim12dALT  908  biorfi  935  pm2.63  937  pm2.8  969  19.30  1885  19.33b  1889  r19.30  3265  r19.30OLD  3266  soxp  7941  xnn0nnn0pnf  12248  iccpnfcnv  24013  elpreq  30779  xlt2addrd  30983  xrge0iifcnv  31785  expdioph  40761  pm10.57  41878  vk15.4j  42037  vk15.4jVD  42423  sineq0ALT  42446  xrnmnfpnf  42522  disjinfi  42620  xrlexaddrp  42781  xrred  42794  xrnpnfmnf  42905  sumnnodd  43061  stoweidlem39  43470  dirkercncflem2  43535  fourierdlem101  43638  fourierswlem  43661  salexct  43763