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

Theorem orci 403
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
Hypothesis
Ref Expression
orci.1 𝜑
Assertion
Ref Expression
orci (𝜑𝜓)

Proof of Theorem orci
StepHypRef Expression
1 orci.1 . . 3 𝜑
21pm2.24i 144 . 2 𝜑𝜓)
32orri 389 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wo 381
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 195  df-or 383
This theorem is referenced by:  truorfal  1501  prid1g  4234  isso2i  4977  0wdom  8331  nneo  11289  mnfltpnf  11793  bcpasc  12921  isumless  14358  binomfallfaclem2  14552  lcmfunsnlem2lem1  15131  srabase  18941  sraaddg  18942  sramulr  18943  m2detleib  20194  fctop  20556  cctop  20558  ovoliunnul  22995  vitalilem5  23100  logtayl  24119  bpos1  24721  usgraexmpldifpr  25690  inindif  28540  disjunsn  28591  ifpimimb  36667  ifpimim  36672  binomcxplemnn0  37369  binomcxplemnotnn0  37376  salexct  39028  onenotinotbothi  39549  twonotinotbothi  39550  clifte  39551  cliftet  39552  pthdlem2  40972  zlmodzxzldeplem  42079  ldepslinc  42090  alimp-surprise  42294  aacllem  42315
  Copyright terms: Public domain W3C validator