Theorem olci 405

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
olci	⊢ (𝜓 ∨ 𝜑)

Proof of Theorem olci

Step	Hyp	Ref	Expression
1		orci.1	. . 3 ⊢ 𝜑
2	1	a1i 11	. 2 ⊢ (¬ 𝜓 → 𝜑)
3	2	orri 390	1 ⊢ (𝜓 ∨ 𝜑)

Syntax hints:  ¬ wn 3   ∨ 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:  falortru  1503  sucidg  5720  kmlem2  8856  sornom  8982  leid  10012  pnf0xnn0  11247  xrleid  11859  xmul01  11969  bcn1  12962  odd2np1lem  14902  lcm0val  15145  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  coprmprod  15213  coprmproddvdslem  15214  prmrec  15464  sratset  19005  srads  19007  m2detleib  20256  zclmncvs  22756  itg0  23352  itgz  23353  coemullem  23810  ftalem5  24603  chp1  24693  prmorcht  24704  pclogsum  24740  logexprlim  24750  bpos1  24808  pntpbnd1  25075  axlowdimlem16  25637  usgraexmpldifpr  25928  cusgrasizeindb1  26000  vdgrf  26425  ex-or  26670  plymulx0  29950  bj-0eltag  32159  bj-inftyexpidisj  32274  mblfinlem2  32617  volsupnfl  32624  ifpdfor  36828  ifpim1  36832  ifpnot  36833  ifpid2  36834  ifpim2  36835  ifpim1g  36865  ifpbi1b  36867  icccncfext  38773  fourierdlem103  39102  fourierdlem104  39103  etransclem24  39151  etransclem35  39162  abnotataxb  39732  dandysum2p2e4  39814  cusgrsizeindb1  40666  pthdlem2  40974  clwwlksn0  41214  zlmodzxzldeplem  42081  aacllem  42356