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

Theorem orci 845
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 147 . 2 𝜑𝜓)
32orri 842 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wo 826
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 827
This theorem is referenced by:  truorfal  1658  prid1g  4429  isso2i  5202  0wdom  8630  nneo  11662  mnfltpnf  12164  bcpasc  13311  isumless  14783  binomfallfaclem2  14976  lcmfunsnlem2lem1  15558  srabase  19392  sraaddg  19393  sramulr  19394  m2detleib  20654  fctop  21028  cctop  21030  ovoliunnul  23494  vitalilem5  23599  logtayl  24626  bpos1  25228  usgrexmpldifpr  26372  cffldtocusgr  26577  pthdlem2  26898  inindif  29685  disjunsn  29739  circlemethhgt  31055  ifpimimb  38368  ifpimim  38373  binomcxplemnn0  39067  binomcxplemnotnn0  39074  salexct  41063  onenotinotbothi  41614  twonotinotbothi  41615  clifte  41616  cliftet  41617  sbgoldbo  42193  zlmodzxzldeplem  42805  ldepslinc  42816  alimp-surprise  43047  aacllem  43068
  Copyright terms: Public domain W3C validator