Theorem olci 406

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

Syntax hints:  ¬ wn 3   ∨ wo 383

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 385

This theorem is referenced by:  falortru  1509  sucidg  5772  kmlem2  8933  sornom  9059  leid  10093  pnf0xnn0  11330  xrleid  11943  xmul01  12056  bcn1  13056  odd2np1lem  15007  lcm0val  15250  lcmfunsnlem2lem1  15294  lcmfunsnlem2  15296  coprmprod  15318  coprmproddvdslem  15319  prmrec  15569  sratset  19124  srads  19126  m2detleib  20377  zclmncvs  22888  itg0  23486  itgz  23487  coemullem  23944  ftalem5  24737  chp1  24827  prmorcht  24838  pclogsum  24874  logexprlim  24884  bpos1  24942  pntpbnd1  25209  axlowdimlem16  25771  usgrexmpldifpr  26077  cusgrsizeindb1  26267  pthdlem2  26567  clwwlksn0  26807  ex-or  27166  plymulx0  30446  bj-0eltag  32666  bj-inftyexpidisj  32769  mblfinlem2  33118  volsupnfl  33125  ifpdfor  37329  ifpim1  37333  ifpnot  37334  ifpid2  37335  ifpim2  37336  ifpim1g  37366  ifpbi1b  37368  icccncfext  39435  fourierdlem103  39763  fourierdlem104  39764  etransclem24  39812  etransclem35  39823  abnotataxb  40417  dandysum2p2e4  40499  zlmodzxzldeplem  41605  aacllem  41880