Theorem pm2.53 852

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

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

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 849

This theorem is referenced by:  jaoi  858  mtord  880  orel1  889  orim12dALT  912  biorfriOLD  941  pm2.63  943  pm2.8  975  19.30  1883  19.33b  1887  r19.30  3105  soxp  8072  xnn0nnn0pnf  12514  iccpnfcnv  24921  nnsge1  28349  elpreq  32613  xlt2addrd  32847  xrge0iifcnv  34093  expdioph  43469  pm10.57  44816  vk15.4j  44973  vk15.4jVD  45358  sineq0ALT  45381  xrnmnfpnf  45532  disjinfi  45640  xrlexaddrp  45800  xrred  45812  xrnpnfmnf  45920  sumnnodd  46078  stoweidlem39  46485  dirkercncflem2  46550  fourierdlem101  46653  fourierswlem  46676  salexct  46780