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

Theorem orel1 886
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 848 . 2 ((𝜑𝜓) → (¬ 𝜑𝜓))
21com12 32 1 𝜑 → ((𝜑𝜓) → 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 844
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 206  df-or 845
This theorem is referenced by:  pm2.25  887  biorf  934  3orel1  1090  xpcan  6079  funun  6480  sorpssuni  7585  sorpssint  7586  soxp  7970  ackbij1lem18  9993  ackbij1b  9995  fincssdom  10079  fin23lem30  10098  fin1a2lem13  10168  pythagtriplem4  16520  zringlpirlem3  20686  psgnodpm  20793  orngsqr  31503  elzdif0  31930  qqhval2lem  31931  eulerpartlemsv2  32325  eulerpartlemv  32331  eulerpartlemf  32337  eulerpartlemgh  32345  3orel13  33660  dfon2lem4  33762  dfon2lem6  33764  frxp3  33797  nosepdmlem  33886  dfrdg4  34253  rankeq1o  34473  wl-orel12  35670  poimirlem31  35808  pellfund14gap  40709  wepwsolem  40867  fmul01lt1lem1  43125  cncfiooicclem1  43434  etransclem24  43799  nnfoctbdjlem  43993
  Copyright terms: Public domain W3C validator