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  1882  19.33b  1886  r19.30  3100  soxp  8068  xnn0nnn0pnf  12478  iccpnfcnv  24889  nnsge1  28291  elpreq  32529  xlt2addrd  32767  xrge0iifcnv  34018  expdioph  43180  pm10.57  44528  vk15.4j  44685  vk15.4jVD  45070  sineq0ALT  45093  xrnmnfpnf  45244  disjinfi  45352  xrlexaddrp  45513  xrred  45525  xrnpnfmnf  45634  sumnnodd  45792  stoweidlem39  46199  dirkercncflem2  46264  fourierdlem101  46367  fourierswlem  46390  salexct  46494