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

Theorem orci 390
 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 376 1
 Colors of variables: wff setvar class Syntax hints:  \/wo 368 This theorem is referenced by:  truorfal  1424  prid1g  4136  isso2i  4837  0wdom  8017  nneo  10971  mnfltpnf  11364  bcpasc  12399  isumless  13657  srabase  17824  sraaddg  17825  sramulr  17826  m2detleib  19133  fctop  19505  cctop  19507  ovoliunnul  21918  vitalilem5  22021  logtayl  23041  bpos1  23558  usgraexmpldifpr  24400  inindif  27414  disjunsn  27453  binomfallfaclem2  29162  binomcxplemnn0  31254  binomcxplemnotnn0  31261  zlmodzxzldeplem  33099  ldepslinc  33110  alimp-surprise  33195  aacllem  33216  bj-ifimimb  37715  bj-ifimim  37716 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 185  df-or 370
 Copyright terms: Public domain W3C validator