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  1076  prel12OLD  4527  xpcan  5728  funun  6093  sorpssuni  7112  sorpssint  7113  soxp  7459  ackbij1lem18  9271  ackbij1b  9273  fincssdom  9357  fin23lem30  9376  fin1a2lem13  9446  pythagtriplem4  15746  evlslem3  19736  zringlpirlem3  20056  psgnodpm  20156  orngsqr  30134  elzdif0  30354  qqhval2lem  30355  eulerpartlemsv2  30750  eulerpartlemv  30756  eulerpartlemf  30762  eulerpartlemgh  30770  3orel13  31926  dfon2lem4  32017  dfon2lem6  32019  nosepdmlem  32160  dfrdg4  32385  rankeq1o  32605  wl-orel12  33625  poimirlem31  33771  pellfund14gap  37971  wepwsolem  38132  fmul01lt1lem1  40337  cncfiooicclem1  40627  etransclem24  40996  nnfoctbdjlem  41193
 Copyright terms: Public domain W3C validator