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  6180  funun  6606  sorpssuni  7772  sorpssint  7773  soxp  8168  frxp3  8195  ackbij1lem18  10341  ackbij1b  10343  fincssdom  10428  fin23lem30  10447  fin1a2lem13  10517  pythagtriplem4  17026  orngsqr  21153  zringlpirlem3  21800  psgnodpm  21924  nosepdmlem  28070  0elold  28326  bdayfinbndlem1  28883  elzdif0  34682  qqhval2lem  34683  eulerpartlemsv2  35060  eulerpartlemv  35066  eulerpartlemf  35072  eulerpartlemgh  35080  maxssj0  36006  dfon2lem4  36726  dfon2lem6  36728  dfrdg4  36893  rankeq1o  37110  wl-orel12  38635  poimirlem31  38761  pellfund14gap  44087  wepwsolem  44242  fmul01lt1lem1  46801  cncfiooicclem1  47108  etransclem24  47473  nnfoctbdjlem  47670