Theorem olci 863

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

Syntax hints:  ¬ wn 3   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  falortru  1577  opthhausdorff  5372  sucidg  6237  kmlem2  9562  sornom  9688  leid  10725  pnf0xnn0  11962  xrleid  12532  xmul01  12648  bcn1  13669  odd2np1lem  15681  lcm0val  15928  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  coprmprod  15995  coprmproddvdslem  15996  prmrec  16248  smndex2dnrinv  18072  sratset  19949  srads  19951  m2detleib  21236  zclmncvs  23753  itg0  24383  itgz  24384  coemullem  24847  ftalem5  25662  chp1  25752  prmorcht  25763  pclogsum  25799  logexprlim  25809  bpos1  25867  addsqnreup  26027  pntpbnd1  26170  axlowdimlem16  26751  usgrexmpldifpr  27048  cusgrsizeindb1  27240  pthdlem2  27557  ex-or  28206  plymulx0  31927  signstfvn  31949  bj-0eltag  34414  bj-inftyexpidisj  34625  mblfinlem2  35095  volsupnfl  35102  12gcd5e1  39291  3lexlogpow5ineq2  39342  ifpdfor  40173  ifpim1  40177  ifpnot  40178  ifpid2  40179  ifpim2  40180  ifpim1g  40209  ifpbi1b  40211  icccncfext  42529  fourierdlem103  42851  fourierdlem104  42852  etransclem24  42900  etransclem35  42911  abnotataxb  43509  dandysum2p2e4  43591  paireqne  44028  sbgoldbo  44305  zlmodzxzldeplem  44907  line2x  45168  aacllem  45329