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

Step	Hyp	Ref	Expression
1		orci.1	. . 3
2	1	pm2.24i 144	. 2
3	2	orri 376	1

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