Theorem orel1 902

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)

Assertion

Ref	Expression
orel1	⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))

Proof of Theorem orel1

Step	Hyp	Ref	Expression
1		pm2.53 865	. 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
2	1	com12 33	1 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm2.25  903  biorf  950  3orel1  1107  3orel13  1518  xpcan  6167  funun  6578  sorpssuni  7737  sorpssint  7738  soxp  8130  frxp3  8152  ackbij1lem18  10295  ackbij1b  10297  fincssdom  10382  fin23lem30  10401  fin1a2lem13  10471  pythagtriplem4  16977  orngsqr  21103  zringlpirlem3  21750  psgnodpm  21874  nosepdmlem  28022  0elold  28278  bdayfinbndlem1  28835  elzdif0  34594  qqhval2lem  34595  eulerpartlemsv2  34973  eulerpartlemv  34979  eulerpartlemf  34985  eulerpartlemgh  34993  dfon2lem4  36518  dfon2lem6  36520  dfrdg4  36685  rankeq1o  36902  wl-orel12  38411  poimirlem31  38537  pellfund14gap  43847  wepwsolem  44002  fmul01lt1lem1  46540  cncfiooicclem1  46847  etransclem24  47212  nnfoctbdjlem  47409