Theorem olcd 888

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30883. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
orcd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
olcd	⊢ (𝜑 → (𝜒 ∨ 𝜓))

Proof of Theorem olcd

Step	Hyp	Ref	Expression
1		orcd.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	orcd 887	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
3	2	orcomd 885	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm2.48  898  pm2.49  899  orim12i  922  pm1.5  933  animorr  994  animorlr  995  cases2ALT  1064  2nreu  4402  2reu4lem  4479  n0snor2el  4793  disjord  5092  propeqop  5484  somin1  6127  nf1const  7305  soxp  8127  xpord2indlem  8145  naddcllem  8664  fowdom  9543  unxpwdom2  9560  nelaneqOLDOLD  9576  djuunxp  9926  fin1a2lem11  10412  axdc3lem2  10453  gchdomtri  10638  hargch  10682  alephgch  10683  nn1m1nn  12278  nn01to3  12990  rpneg  13076  ltpnf  13171  mnflt  13174  xrlttri  13190  xmulpnf1  13326  iccsplit  13538  elfznelfzo  13829  fvf1tp  13850  addmodlteq  14010  bc0k  14375  bcpasc  14385  hashv01gt1  14409  hashrabsn01  14437  hashsn01  14481  pr2pwpr  14544  hashtpg  14550  ccatsymb  14648  s3sndisj  15040  s3iunsndisj  15041  fsum  15806  fsumsplit  15827  fprod  16028  binomfallfaclem2  16126  fsumdvds  16398  pwp1fsum  16481  lcmfunsnlem1  16727  lcmfunsnlem2  16730  2mulprm  16783  ncoprmlnprm  16819  4sqlem17  17053  vdwlem6  17078  ram0  17114  cshwsidrepswmod0  17186  cshwsdisj  17190  basprssdmsets  17313  mreexfidimd  17738  homffval  17778  comfffval  17786  natfval  18038  xpchomfval  18267  xpccofval  18270  chnccat  18714  plusffval  18736  efmndplusg  18989  smndex1mgm  19019  sgrp2nmndlem5  19041  grpsubfval  19107  grpsubfvalALT  19108  psgnunilem1  19620  psgnunilem5  19621  gsummulg  20069  prmgrpsimpgd  20243  srgbinomlem3  20367  lringuplu  20706  scaffval  21064  drngnidl  21440  cnsubrg  21640  ipffval  21861  lindsdom  22063  psrmulr  22157  pmatcoe1fsupp  22926  en2top  23210  fctop  23229  cctop  23231  metustto  24779  pcofval  25238  pmltpclem2  25677  itg1addlem5  25928  itg10a  25938  dvne0  26238  plyeq0lem  26436  plymullem1  26440  aalioulem4  26571  aalioulem5  26572  aaliou2b  26577  ang180lem3  27048  basellem2  27318  musumsum  27428  dchrhash  27507  lgsdir2lem5  27565  rpvmasumlem  27723  rpvmasum2  27748  pntlemj  27839  ltsres  27898  noetainflem4  27976  addsval  28227  mulsval  28374  mulsproplem13  28393  mulsproplem14  28394  n0s0suc  28607  n0s0m1  28627  nn1m1nns  28639  zseo  28687  halfcut  28723  bdayfinbndlem1  28732  z12zsodd  28747  tgbtwnconn1  28917  tgbtwnconn2  28918  hlid  28954  hltr  28955  hlbtwn  28956  lnhl  28960  colmid  29039  hlpasch  29113  lnincplng  29141  lmieu  29168  lmiinv  29176  cgrahl  29214  cgracol  29215  inaghl  29243  prlngd  29296  edglnl  29600  umgrvad2edg  29673  nbgrnvtx0  29799  wwlksnfi  30374  clwlkclwwlklem2a  30468  clwwlknnn  30503  clwwlknon1nloop  30569  eupth2lem2  30699  frgrwopreg  30803  2wspmdisj  30817  frgrreg  30874  ex-natded5.7  30891  ex-natded5.13  30895  ex-natded9.20  30897  ex-natded9.20-2  30898  aevdemo  30940  f1ocnt  33271  linds2eq  33814  constrextdg2lem  34258  esumsnf  34574  meascnbl  34730  signsplypnf  35058  hashreprin  35128  circlemeth  35148  satfvsucsuc  35944  fmlasucdisj  35978  satfun  35990  satfv1fvfmla1  36002  2goelgoanfmla1  36003  dfrdg4  36530  outsideoftr  36709  lineunray  36727  weiunpo  37084  weiunso  37085  ftc1anclem3  38444  dvasin  38453  areacirclem4  38460  smprngopr  38802  tsbi1  38881  tsbi2  38882  lkrshpor  39980  cdleme22b  41214  tendoex  41848  lcfrlem9  42423  aks6d1c2p2  42985  hashnexinjle  42995  grpods  43060  unitscyglem2  43062  pell1234qrdich  43702  acongtr  43819  acongrep  43821  jm2.23  43837  jm2.25  43840  fnwe2lem3  43893  kelac2lem  43905  mendplusgfval  44022  mendmulrfval  44024  onmcl  44172  fzunt  44295  fzuntd  44296  fzunt1d  44297  fzuntgd  44298  ifpim23g  44335  frege122d  44600  clsk1indlem3  44883  refsum2cnlem1  45871  disjxp1  45903  eliuniincex  45941  eliincex  45942  fmul01lt1lem1  46414  limciccioolb  46451  sumnnodd  46460  limcicciooub  46465  wallispilem3  46895  fourierdlem35  46970  fourierdlem80  47014  fourierdlem101  47035  fourierswlem  47058  etransclem32  47094  etransclem35  47097  nnfoctbdjlem  47283  numtowerdt  47734  otiunsndisjX  48167  nltle2tri  48201  icceuelpartlem  48335  lighneallem3  48510  evennodd  48559  oddneven  48560  clnbgrnvtx0  48743  predgclnbgrel  48755  clnbgredg  48756  vopnbgrelself  48771  dfclnbgr6  48772  dfsclnbgr6  48774  clnbgrgrimlem  48849  clnbgrgrim  48850  grlimprclnbgr  48912  usgrexmpl2trifr  48953  gpgusgralem  48972  gpg5nbgrvtx03starlem1  48984  gpg5nbgrvtx03starlem2  48985  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx13starlem1  48987  gpg5nbgrvtx13starlem2  48988  gpg5nbgrvtx13starlem3  48989  gpg3nbgrvtx0  48992  gpg3nbgrvtx0ALT  48993  gpg3nbgrvtx1  48994  gpg3kgrtriex  49005  gpg5edgnedg  49046  smprngprmrng  49254  altgsumbcALT  49283  lindslinindsimp1  49387  lindszr  49399  zlmodzxznm  49427  elfzolborelfzop1  49449  blen1b  49518  reorelicc  49640  prelrrx2b  49644  inlinecirc02plem  49716  fvconst0ci  49817