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  6179  funun  6589  sorpssuni  7742  sorpssint  7743  soxp  8134  frxp3  8156  ackbij1lem18  10238  ackbij1b  10240  fincssdom  10325  fin23lem30  10344  fin1a2lem13  10414  pythagtriplem4  16904  orngsqr  21006  zringlpirlem3  21651  psgnodpm  21775  nosepdmlem  27884  0elold  28140  bdayfinbndlem1  28697  elzdif0  34401  qqhval2lem  34402  eulerpartlemsv2  34780  eulerpartlemv  34786  eulerpartlemf  34792  eulerpartlemgh  34800  dfon2lem4  36297  dfon2lem6  36299  dfrdg4  36464  rankeq1o  36684  wl-orel12  38207  poimirlem31  38343  pellfund14gap  43655  wepwsolem  43810  fmul01lt1lem1  46341  cncfiooicclem1  46648  etransclem24  47013  nnfoctbdjlem  47210