Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30389. (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 873	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
3	2	orcomd 871	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  pm2.48  884  pm2.49  885  orim12i  908  pm1.5  919  animorr  980  animorlr  981  cases2ALT  1048  2nreu  4424  2reu4lem  4502  n0snor2el  4814  disjord  5113  propeqop  5487  somin1  6127  nf1const  7302  soxp  8133  xpord2indlem  8151  naddcllem  8693  fowdom  9590  unxpwdom2  9607  nelaneq  9618  djuunxp  9940  fin1a2lem11  10429  axdc3lem2  10470  gchdomtri  10648  hargch  10692  alephgch  10693  nn1m1nn  12266  nn01to3  12962  rpneg  13046  ltpnf  13141  mnflt  13144  xrlttri  13160  xmulpnf1  13295  iccsplit  13507  elfznelfzo  13793  fvf1tp  13811  addmodlteq  13969  bc0k  14334  bcpasc  14344  hashv01gt1  14368  hashrabsn01  14396  hashsn01  14439  pr2pwpr  14502  hashtpg  14508  ccatsymb  14605  s3sndisj  14991  s3iunsndisj  14992  fsum  15741  fsumsplit  15762  fprod  15962  binomfallfaclem2  16061  fsumdvds  16332  pwp1fsum  16415  lcmfunsnlem1  16661  lcmfunsnlem2  16664  2mulprm  16717  ncoprmlnprm  16752  4sqlem17  16986  vdwlem6  17011  ram0  17047  cshwsidrepswmod0  17119  cshwsdisj  17123  basprssdmsets  17245  mreexfidimd  17667  homffval  17707  comfffval  17715  natfval  17967  xpchomfval  18196  xpccofval  18199  plusffval  18629  efmndplusg  18863  smndex1mgm  18890  sgrp2nmndlem5  18912  grpsubfval  18971  grpsubfvalALT  18972  psgnunilem1  19479  psgnunilem5  19480  gsummulg  19928  prmgrpsimpgd  20102  srgbinomlem3  20193  lringuplu  20509  scaffval  20842  drngnidl  21209  cnsubrg  21400  ipffval  21613  psrmulr  21907  pmatcoe1fsupp  22644  en2top  22928  fctop  22947  cctop  22949  metustto  24497  pcofval  24966  pmltpclem2  25407  itg1addlem5  25658  itg10a  25668  dvne0  25973  plyeq0lem  26172  plymullem1  26176  aalioulem4  26300  aalioulem5  26301  aaliou2b  26306  ang180lem3  26778  basellem2  27049  musumsum  27159  dchrhash  27239  lgsdir2lem5  27297  rpvmasumlem  27455  rpvmasum2  27480  pntlemj  27571  sltres  27631  noetainflem4  27709  addsval  27926  mulsval  28069  mulsproplem13  28088  mulsproplem14  28089  n0s0suc  28291  n0s0m1  28309  nn1m1nns  28320  zseo  28365  halfcut  28390  tgbtwnconn1  28559  tgbtwnconn2  28560  hlid  28593  hltr  28594  hlbtwn  28595  lnhl  28599  colmid  28672  hlpasch  28740  lmieu  28768  lmiinv  28776  cgrahl  28811  cgracol  28812  inaghl  28829  edglnl  29127  umgrvad2edg  29197  nbgrnvtx0  29323  wwlksnfi  29893  clwlkclwwlklem2a  29984  clwwlknnn  30019  clwwlknon1nloop  30085  eupth2lem2  30205  frgrwopreg  30309  2wspmdisj  30323  frgrreg  30380  ex-natded5.7  30397  ex-natded5.13  30401  ex-natded9.20  30403  ex-natded9.20-2  30404  aevdemo  30446  f1ocnt  32784  linds2eq  33401  constrextdg2lem  33787  esumsnf  34100  meascnbl  34255  signsplypnf  34587  hashreprin  34657  circlemeth  34677  satfvsucsuc  35392  fmlasucdisj  35426  satfun  35438  satfv1fvfmla1  35450  2goelgoanfmla1  35451  dfrdg4  35974  outsideoftr  36152  lineunray  36170  weiunpo  36488  weiunso  36489  lindsdom  37643  ftc1anclem3  37724  dvasin  37733  areacirclem4  37740  smprngopr  38081  tsbi1  38162  tsbi2  38163  lkrshpor  39130  cdleme22b  40365  tendoex  40999  lcfrlem9  41574  aks6d1c2p2  42137  hashnexinjle  42147  grpods  42212  unitscyglem2  42214  pell1234qrdich  42859  acongtr  42977  acongrep  42979  jm2.23  42995  jm2.25  42998  fnwe2lem3  43051  kelac2lem  43063  mendplusgfval  43180  mendmulrfval  43182  onmcl  43330  fzunt  43454  fzuntd  43455  fzunt1d  43456  fzuntgd  43457  ifpim23g  43494  frege122d  43759  clsk1indlem3  44042  refsum2cnlem1  45041  disjxp1  45073  eliuniincex  45113  eliincex  45114  fmul01lt1lem1  45593  limciccioolb  45630  sumnnodd  45639  limcicciooub  45646  wallispilem3  46076  fourierdlem35  46151  fourierdlem80  46195  fourierdlem101  46216  fourierswlem  46239  etransclem32  46275  etransclem35  46278  nnfoctbdjlem  46464  squeezedltsq  46898  otiunsndisjX  47288  nltle2tri  47322  icceuelpartlem  47429  lighneallem3  47601  evennodd  47637  oddneven  47638  clnbgrnvtx0  47821  predgclnbgrel  47832  clnbgredg  47833  vopnbgrelself  47848  dfclnbgr6  47849  dfsclnbgr6  47851  clnbgrgrimlem  47926  clnbgrgrim  47927  usgrexmpl2trifr  48021  gpgusgralem  48040  gpg5nbgrvtx03starlem1  48050  gpg5nbgrvtx03starlem2  48051  gpg5nbgrvtx03starlem3  48052  gpg5nbgrvtx13starlem1  48053  gpg5nbgrvtx13starlem2  48054  gpg5nbgrvtx13starlem3  48055  gpg3nbgrvtx0  48058  gpg3nbgrvtx0ALT  48059  gpg3nbgrvtx1  48060  gpg3kgrtriex  48071  altgsumbcALT  48308  lindslinindsimp1  48413  lindszr  48425  zlmodzxznm  48453  elfzolborelfzop1  48475  blen1b  48548  reorelicc  48670  prelrrx2b  48674  inlinecirc02plem  48746  fvconst0ci  48846