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

Theorem orel1 913
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 878 . 2 ((𝜑𝜓) → (¬ 𝜑𝜓))
21com12 32 1 𝜑 → ((𝜑𝜓) → 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 874
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 199  df-or 875
This theorem is referenced by:  pm2.25  914  biorf  961  3orel1  1112  prel12OLD  4568  xpcan  5787  funun  6146  sorpssuni  7180  sorpssint  7181  soxp  7527  ackbij1lem18  9347  ackbij1b  9349  fincssdom  9433  fin23lem30  9452  fin1a2lem13  9522  pythagtriplem4  15857  evlslem3  19836  zringlpirlem3  20156  psgnodpm  20255  orngsqr  30320  elzdif0  30540  qqhval2lem  30541  eulerpartlemsv2  30936  eulerpartlemv  30942  eulerpartlemf  30948  eulerpartlemgh  30956  3orel13  32113  dfon2lem4  32203  dfon2lem6  32205  nosepdmlem  32346  dfrdg4  32571  rankeq1o  32791  wl-orel12  33792  poimirlem31  33929  pellfund14gap  38233  wepwsolem  38393  fmul01lt1lem1  40556  cncfiooicclem1  40846  etransclem24  41214  nnfoctbdjlem  41411
  Copyright terms: Public domain W3C validator