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

Theorem orci 405
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 146 . 2 𝜑𝜓)
32orri 391 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wo 383
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 385
This theorem is referenced by:  truorfal  1510  prid1g  4293  isso2i  5065  0wdom  8472  nneo  11458  mnfltpnf  11957  bcpasc  13103  isumless  14571  binomfallfaclem2  14765  lcmfunsnlem2lem1  15345  srabase  19172  sraaddg  19173  sramulr  19174  m2detleib  20431  fctop  20802  cctop  20804  ovoliunnul  23269  vitalilem5  23375  logtayl  24400  bpos1  25002  usgrexmpldifpr  26144  cffldtocusgr  26337  pthdlem2  26658  inindif  29337  disjunsn  29391  circlemethhgt  30706  ifpimimb  37675  ifpimim  37680  binomcxplemnn0  38374  binomcxplemnotnn0  38381  salexct  40321  onenotinotbothi  40869  twonotinotbothi  40870  clifte  40871  cliftet  40872  sbgoldbo  41446  zlmodzxzldeplem  42058  ldepslinc  42069  alimp-surprise  42297  aacllem  42318
  Copyright terms: Public domain W3C validator