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

Theorem orel1 888
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 850 . 2 ((𝜑𝜓) → (¬ 𝜑𝜓))
21com12 32 1 𝜑 → ((𝜑𝜓) → 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 846
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 210  df-or 847
This theorem is referenced by:  pm2.25  889  biorf  936  3orel1  1092  xpcan  6008  funun  6385  sorpssuni  7476  sorpssint  7477  soxp  7849  ackbij1lem18  9737  ackbij1b  9739  fincssdom  9823  fin23lem30  9842  fin1a2lem13  9912  pythagtriplem4  16256  zringlpirlem3  20305  psgnodpm  20404  orngsqr  31080  elzdif0  31500  qqhval2lem  31501  eulerpartlemsv2  31895  eulerpartlemv  31901  eulerpartlemf  31907  eulerpartlemgh  31915  3orel13  33233  dfon2lem4  33334  dfon2lem6  33336  frxp3  33408  nosepdmlem  33527  dfrdg4  33891  rankeq1o  34111  wl-orel12  35293  poimirlem31  35431  pellfund14gap  40281  wepwsolem  40439  fmul01lt1lem1  42667  cncfiooicclem1  42976  etransclem24  43341  nnfoctbdjlem  43535
  Copyright terms: Public domain W3C validator