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

Theorem orel1 396
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 387 . 2 ((𝜑𝜓) → (¬ 𝜑𝜓))
21com12 32 1 𝜑 → ((𝜑𝜓) → 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382
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 197  df-or 384
This theorem is referenced by:  pm2.25  418  biorf  419  3orel1  1058  prel12  4414  xpcan  5605  funun  5970  sorpssuni  6988  sorpssint  6989  soxp  7335  ackbij1lem18  9097  ackbij1b  9099  fincssdom  9183  fin23lem30  9202  fin1a2lem13  9272  pythagtriplem4  15571  evlslem3  19562  zringlpirlem3  19882  psgnodpm  19982  orngsqr  29932  elzdif0  30152  qqhval2lem  30153  eulerpartlemsv2  30548  eulerpartlemv  30554  eulerpartlemf  30560  eulerpartlemgh  30568  3orel13  31724  dfon2lem4  31815  dfon2lem6  31817  nosepdmlem  31958  dfrdg4  32183  rankeq1o  32403  wl-orel12  33424  poimirlem31  33570  pellfund14gap  37768  wepwsolem  37929  fmul01lt1lem1  40134  cncfiooicclem1  40424  etransclem24  40793  nnfoctbdjlem  40990
  Copyright terms: Public domain W3C validator