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  1517  xpcan  6167  funun  6586  sorpssuni  7748  sorpssint  7749  soxp  8143  frxp3  8170  ackbij1lem18  10317  ackbij1b  10319  fincssdom  10404  fin23lem30  10423  fin1a2lem13  10493  pythagtriplem4  17002  orngsqr  21128  zringlpirlem3  21775  psgnodpm  21899  nosepdmlem  28045  0elold  28301  bdayfinbndlem1  28858  elzdif0  34658  qqhval2lem  34659  eulerpartlemsv2  35036  eulerpartlemv  35042  eulerpartlemf  35048  eulerpartlemgh  35056  maxssj0  35945  dfon2lem4  36640  dfon2lem6  36642  dfrdg4  36807  rankeq1o  37024  wl-orel12  38536  poimirlem31  38662  pellfund14gap  43987  wepwsolem  44142  fmul01lt1lem1  46689  cncfiooicclem1  46996  etransclem24  47361  nnfoctbdjlem  47558