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  3100  soxp  8085  xnn0nnn0pnf  12504  iccpnfcnv  24818  nnsge1  28211  elpreq  32430  xlt2addrd  32655  xrge0iifcnv  33896  expdioph  42985  pm10.57  44333  vk15.4j  44491  vk15.4jVD  44876  sineq0ALT  44899  xrnmnfpnf  45050  disjinfi  45159  xrlexaddrp  45321  xrred  45334  xrnpnfmnf  45443  sumnnodd  45601  stoweidlem39  46010  dirkercncflem2  46075  fourierdlem101  46178  fourierswlem  46201  salexct  46305