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

Theorem orci 404
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 145 . 2 𝜑𝜓)
32orri 390 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  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 196  df-or 384
This theorem is referenced by:  truorfal  1502  prid1g  4239  isso2i  4991  0wdom  8358  nneo  11337  mnfltpnf  11836  bcpasc  12970  isumless  14416  binomfallfaclem2  14610  lcmfunsnlem2lem1  15189  srabase  18999  sraaddg  19000  sramulr  19001  m2detleib  20256  fctop  20618  cctop  20620  ovoliunnul  23082  vitalilem5  23187  logtayl  24206  bpos1  24808  usgraexmpldifpr  25928  inindif  28738  disjunsn  28789  ifpimimb  36868  ifpimim  36873  binomcxplemnn0  37570  binomcxplemnotnn0  37577  salexct  39228  onenotinotbothi  39749  twonotinotbothi  39750  clifte  39751  cliftet  39752  pthdlem2  40974  zlmodzxzldeplem  42081  ldepslinc  42092  alimp-surprise  42335  aacllem  42356
  Copyright terms: Public domain W3C validator