Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  orel1 Structured version   Visualization version   GIF version

Theorem orel1 885
 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
StepHypRef Expression
1 pm2.53 847 . 2 ((𝜑𝜓) → (¬ 𝜑𝜓))
21com12 32 1 𝜑 → ((𝜑𝜓) → 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 843 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 844 This theorem is referenced by:  pm2.25  886  biorf  933  3orel1  1087  xpcan  6032  funun  6399  sorpssuni  7457  sorpssint  7458  soxp  7822  ackbij1lem18  9658  ackbij1b  9660  fincssdom  9744  fin23lem30  9763  fin1a2lem13  9833  pythagtriplem4  16155  zringlpirlem3  20632  psgnodpm  20731  orngsqr  30877  elzdif0  31221  qqhval2lem  31222  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemf  31628  eulerpartlemgh  31636  3orel13  32947  dfon2lem4  33031  dfon2lem6  33033  nosepdmlem  33187  dfrdg4  33412  rankeq1o  33632  wl-orel12  34750  poimirlem31  34922  pellfund14gap  39482  wepwsolem  39640  fmul01lt1lem1  41863  cncfiooicclem1  42174  etransclem24  42542  nnfoctbdjlem  42736
 Copyright terms: Public domain W3C validator