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

Theorem orci 862
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 150 . 2 𝜑𝜓)
32orri 859 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wo 844
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 206  df-or 845
This theorem is referenced by:  truorfal  1577  trunorfalOLD  1590  prid1g  4696  isso2i  5538  mpo0v  7359  0wdom  9329  nneo  12404  mnfltpnf  12862  bcpasc  14035  isumless  15557  binomfallfaclem2  15750  lcmfunsnlem2lem1  16343  srabaseOLD  20442  sraaddgOLD  20444  sramulrOLD  20446  m2detleib  21780  fctop  22154  cctop  22156  ovoliunnul  24671  vitalilem5  24776  logtayl  25815  bpos1  26431  usgrexmpldifpr  27625  cffldtocusgr  27814  pthdlem2  28136  inindif  30863  disjunsn  30933  circlemethhgt  32623  fmla0disjsuc  33360  0slt1s  34023  ifpimimb  41111  ifpimim  41116  binomcxplemnn0  41967  binomcxplemnotnn0  41974  salexct  43873  onenotinotbothi  44428  twonotinotbothi  44429  clifte  44430  cliftet  44431  paireqne  44963  sbgoldbo  45239  zlmodzxzldeplem  45839  ldepslinc  45850  line2x  46100  inlinecirc02plem  46132  alimp-surprise  46484  aacllem  46505
  Copyright terms: Public domain W3C validator