Theorem orel1 899

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 862	. 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
2	1	com12 32	1 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))

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

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 209  df-or 859

This theorem is referenced by:  pm2.25  900  biorf  947  3orel1  1101  3orel13  1507  xpcan  6156  funun  6561  sorpssuni  7709  sorpssint  7710  soxp  8102  frxp3  8124  ackbij1lem18  10187  ackbij1b  10189  fincssdom  10275  fin23lem30  10294  fin1a2lem13  10364  pythagtriplem4  16836  orngsqr  20893  zringlpirlem3  21494  psgnodpm  21618  nosepdmlem  27722  0elold  27978  bdayfinbndlem1  28535  elzdif0  34236  qqhval2lem  34237  eulerpartlemsv2  34614  eulerpartlemv  34620  eulerpartlemf  34626  eulerpartlemgh  34634  dfon2lem4  36087  dfon2lem6  36089  dfrdg4  36254  rankeq1o  36474  wl-orel12  37967  poimirlem31  38103  pellfund14gap  43417  wepwsolem  43572  fmul01lt1lem1  46113  cncfiooicclem1  46420  etransclem24  46785  nnfoctbdjlem  46982