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  3096  soxp  8069  xnn0nnn0pnf  12489  iccpnfcnv  24859  nnsge1  28259  elpreq  32491  xlt2addrd  32721  xrge0iifcnv  33919  expdioph  43016  pm10.57  44364  vk15.4j  44522  vk15.4jVD  44907  sineq0ALT  44930  xrnmnfpnf  45081  disjinfi  45190  xrlexaddrp  45352  xrred  45364  xrnpnfmnf  45473  sumnnodd  45631  stoweidlem39  46040  dirkercncflem2  46105  fourierdlem101  46208  fourierswlem  46231  salexct  46335