Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30478. (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  4396  2reu4lem  4476  n0snor2el  4789  disjord  5087  propeqop  5455  somin1  6090  nf1const  7250  soxp  8071  xpord2indlem  8089  naddcllem  8604  fowdom  9476  unxpwdom2  9493  nelaneqOLD  9507  djuunxp  9833  fin1a2lem11  10320  axdc3lem2  10361  gchdomtri  10540  hargch  10584  alephgch  10585  nn1m1nn  12166  nn01to3  12854  rpneg  12939  ltpnf  13034  mnflt  13037  xrlttri  13053  xmulpnf1  13189  iccsplit  13401  elfznelfzo  13689  fvf1tp  13709  addmodlteq  13869  bc0k  14234  bcpasc  14244  hashv01gt1  14268  hashrabsn01  14296  hashsn01  14339  pr2pwpr  14402  hashtpg  14408  ccatsymb  14506  s3sndisj  14890  s3iunsndisj  14891  fsum  15643  fsumsplit  15664  fprod  15864  binomfallfaclem2  15963  fsumdvds  16235  pwp1fsum  16318  lcmfunsnlem1  16564  lcmfunsnlem2  16567  2mulprm  16620  ncoprmlnprm  16655  4sqlem17  16889  vdwlem6  16914  ram0  16950  cshwsidrepswmod0  17022  cshwsdisj  17026  basprssdmsets  17148  mreexfidimd  17573  homffval  17613  comfffval  17621  natfval  17873  xpchomfval  18102  xpccofval  18105  chnccat  18549  plusffval  18571  efmndplusg  18805  smndex1mgm  18832  sgrp2nmndlem5  18854  grpsubfval  18913  grpsubfvalALT  18914  psgnunilem1  19422  psgnunilem5  19423  gsummulg  19871  prmgrpsimpgd  20045  srgbinomlem3  20163  lringuplu  20477  scaffval  20831  drngnidl  21198  cnsubrg  21382  ipffval  21603  psrmulr  21898  pmatcoe1fsupp  22645  en2top  22929  fctop  22948  cctop  22950  metustto  24497  pcofval  24966  pmltpclem2  25406  itg1addlem5  25657  itg10a  25667  dvne0  25972  plyeq0lem  26171  plymullem1  26175  aalioulem4  26299  aalioulem5  26300  aaliou2b  26305  ang180lem3  26777  basellem2  27048  musumsum  27158  dchrhash  27238  lgsdir2lem5  27296  rpvmasumlem  27454  rpvmasum2  27479  pntlemj  27570  ltsres  27630  noetainflem4  27708  addsval  27958  mulsval  28105  mulsproplem13  28124  mulsproplem14  28125  n0s0suc  28338  n0s0m1  28358  nn1m1nns  28370  zseo  28418  halfcut  28454  bdayfinbndlem1  28463  z12zsodd  28478  tgbtwnconn1  28647  tgbtwnconn2  28648  hlid  28681  hltr  28682  hlbtwn  28683  lnhl  28687  colmid  28760  hlpasch  28828  lmieu  28856  lmiinv  28864  cgrahl  28899  cgracol  28900  inaghl  28917  edglnl  29216  umgrvad2edg  29286  nbgrnvtx0  29412  wwlksnfi  29979  clwlkclwwlklem2a  30073  clwwlknnn  30108  clwwlknon1nloop  30174  eupth2lem2  30294  frgrwopreg  30398  2wspmdisj  30412  frgrreg  30469  ex-natded5.7  30486  ex-natded5.13  30490  ex-natded9.20  30492  ex-natded9.20-2  30493  aevdemo  30535  f1ocnt  32880  linds2eq  33462  constrextdg2lem  33905  esumsnf  34221  meascnbl  34376  signsplypnf  34707  hashreprin  34777  circlemeth  34797  satfvsucsuc  35559  fmlasucdisj  35593  satfun  35605  satfv1fvfmla1  35617  2goelgoanfmla1  35618  dfrdg4  36145  outsideoftr  36323  lineunray  36341  weiunpo  36659  weiunso  36660  lindsdom  37815  ftc1anclem3  37896  dvasin  37905  areacirclem4  37912  smprngopr  38253  tsbi1  38334  tsbi2  38335  lkrshpor  39367  cdleme22b  40601  tendoex  41235  lcfrlem9  41810  aks6d1c2p2  42373  hashnexinjle  42383  grpods  42448  unitscyglem2  42450  pell1234qrdich  43103  acongtr  43220  acongrep  43222  jm2.23  43238  jm2.25  43241  fnwe2lem3  43294  kelac2lem  43306  mendplusgfval  43423  mendmulrfval  43425  onmcl  43573  fzunt  43696  fzuntd  43697  fzunt1d  43698  fzuntgd  43699  ifpim23g  43736  frege122d  44001  clsk1indlem3  44284  refsum2cnlem1  45282  disjxp1  45314  eliuniincex  45353  eliincex  45354  fmul01lt1lem1  45830  limciccioolb  45867  sumnnodd  45876  limcicciooub  45881  wallispilem3  46311  fourierdlem35  46386  fourierdlem80  46430  fourierdlem101  46451  fourierswlem  46474  etransclem32  46510  etransclem35  46513  nnfoctbdjlem  46699  nthrucw  47130  squeezedltsq  47132  otiunsndisjX  47525  nltle2tri  47559  icceuelpartlem  47681  lighneallem3  47853  evennodd  47889  oddneven  47890  clnbgrnvtx0  48073  predgclnbgrel  48085  clnbgredg  48086  vopnbgrelself  48101  dfclnbgr6  48102  dfsclnbgr6  48104  clnbgrgrimlem  48179  clnbgrgrim  48180  grlimprclnbgr  48242  usgrexmpl2trifr  48283  gpgusgralem  48302  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem2  48318  gpg5nbgrvtx13starlem3  48319  gpg3nbgrvtx0  48322  gpg3nbgrvtx0ALT  48323  gpg3nbgrvtx1  48324  gpg3kgrtriex  48335  gpg5edgnedg  48376  altgsumbcALT  48599  lindslinindsimp1  48703  lindszr  48715  zlmodzxznm  48743  elfzolborelfzop1  48765  blen1b  48834  reorelicc  48956  prelrrx2b  48960  inlinecirc02plem  49032  fvconst0ci  49136