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  1882  19.33b  1886  r19.30  3118  r19.30OLD  3119  soxp  8119  xnn0nnn0pnf  12563  iccpnfcnv  24691  elpreq  32032  xlt2addrd  32236  xrge0iifcnv  33209  expdioph  42066  pm10.57  43434  vk15.4j  43593  vk15.4jVD  43979  sineq0ALT  44002  xrnmnfpnf  44075  disjinfi  44191  xrlexaddrp  44362  xrred  44375  xrnpnfmnf  44485  sumnnodd  44646  stoweidlem39  45055  dirkercncflem2  45120  fourierdlem101  45223  fourierswlem  45246  salexct  45350