Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30383. (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  4391  2reu4lem  4469  n0snor2el  4782  disjord  5078  propeqop  5445  somin1  6079  nf1const  7238  soxp  8059  xpord2indlem  8077  naddcllem  8591  fowdom  9457  unxpwdom2  9474  nelaneqOLD  9488  djuunxp  9814  fin1a2lem11  10301  axdc3lem2  10342  gchdomtri  10520  hargch  10564  alephgch  10565  nn1m1nn  12146  nn01to3  12839  rpneg  12924  ltpnf  13019  mnflt  13022  xrlttri  13038  xmulpnf1  13173  iccsplit  13385  elfznelfzo  13673  fvf1tp  13693  addmodlteq  13853  bc0k  14218  bcpasc  14228  hashv01gt1  14252  hashrabsn01  14280  hashsn01  14323  pr2pwpr  14386  hashtpg  14392  ccatsymb  14490  s3sndisj  14874  s3iunsndisj  14875  fsum  15627  fsumsplit  15648  fprod  15848  binomfallfaclem2  15947  fsumdvds  16219  pwp1fsum  16302  lcmfunsnlem1  16548  lcmfunsnlem2  16551  2mulprm  16604  ncoprmlnprm  16639  4sqlem17  16873  vdwlem6  16898  ram0  16934  cshwsidrepswmod0  17006  cshwsdisj  17010  basprssdmsets  17132  mreexfidimd  17556  homffval  17596  comfffval  17604  natfval  17856  xpchomfval  18085  xpccofval  18088  chnccat  18532  plusffval  18554  efmndplusg  18788  smndex1mgm  18815  sgrp2nmndlem5  18837  grpsubfval  18896  grpsubfvalALT  18897  psgnunilem1  19405  psgnunilem5  19406  gsummulg  19854  prmgrpsimpgd  20028  srgbinomlem3  20146  lringuplu  20459  scaffval  20813  drngnidl  21180  cnsubrg  21364  ipffval  21585  psrmulr  21879  pmatcoe1fsupp  22616  en2top  22900  fctop  22919  cctop  22921  metustto  24468  pcofval  24937  pmltpclem2  25377  itg1addlem5  25628  itg10a  25638  dvne0  25943  plyeq0lem  26142  plymullem1  26146  aalioulem4  26270  aalioulem5  26271  aaliou2b  26276  ang180lem3  26748  basellem2  27019  musumsum  27129  dchrhash  27209  lgsdir2lem5  27267  rpvmasumlem  27425  rpvmasum2  27450  pntlemj  27541  sltres  27601  noetainflem4  27679  addsval  27905  mulsval  28048  mulsproplem13  28067  mulsproplem14  28068  n0s0suc  28270  n0s0m1  28288  nn1m1nns  28299  zseo  28345  halfcut  28378  zs12zodd  28392  tgbtwnconn1  28553  tgbtwnconn2  28554  hlid  28587  hltr  28588  hlbtwn  28589  lnhl  28593  colmid  28666  hlpasch  28734  lmieu  28762  lmiinv  28770  cgrahl  28805  cgracol  28806  inaghl  28823  edglnl  29121  umgrvad2edg  29191  nbgrnvtx0  29317  wwlksnfi  29884  clwlkclwwlklem2a  29978  clwwlknnn  30013  clwwlknon1nloop  30079  eupth2lem2  30199  frgrwopreg  30303  2wspmdisj  30317  frgrreg  30374  ex-natded5.7  30391  ex-natded5.13  30395  ex-natded9.20  30397  ex-natded9.20-2  30398  aevdemo  30440  f1ocnt  32782  linds2eq  33346  constrextdg2lem  33761  esumsnf  34077  meascnbl  34232  signsplypnf  34563  hashreprin  34633  circlemeth  34653  satfvsucsuc  35409  fmlasucdisj  35443  satfun  35455  satfv1fvfmla1  35467  2goelgoanfmla1  35468  dfrdg4  35993  outsideoftr  36171  lineunray  36189  weiunpo  36507  weiunso  36508  lindsdom  37662  ftc1anclem3  37743  dvasin  37752  areacirclem4  37759  smprngopr  38100  tsbi1  38181  tsbi2  38182  lkrshpor  39154  cdleme22b  40388  tendoex  41022  lcfrlem9  41597  aks6d1c2p2  42160  hashnexinjle  42170  grpods  42235  unitscyglem2  42237  pell1234qrdich  42902  acongtr  43019  acongrep  43021  jm2.23  43037  jm2.25  43040  fnwe2lem3  43093  kelac2lem  43105  mendplusgfval  43222  mendmulrfval  43224  onmcl  43372  fzunt  43496  fzuntd  43497  fzunt1d  43498  fzuntgd  43499  ifpim23g  43536  frege122d  43801  clsk1indlem3  44084  refsum2cnlem1  45082  disjxp1  45114  eliuniincex  45154  eliincex  45155  fmul01lt1lem1  45632  limciccioolb  45669  sumnnodd  45678  limcicciooub  45683  wallispilem3  46113  fourierdlem35  46188  fourierdlem80  46232  fourierdlem101  46253  fourierswlem  46276  etransclem32  46312  etransclem35  46315  nnfoctbdjlem  46501  squeezedltsq  46925  otiunsndisjX  47318  nltle2tri  47352  icceuelpartlem  47474  lighneallem3  47646  evennodd  47682  oddneven  47683  clnbgrnvtx0  47866  predgclnbgrel  47878  clnbgredg  47879  vopnbgrelself  47894  dfclnbgr6  47895  dfsclnbgr6  47897  clnbgrgrimlem  47972  clnbgrgrim  47973  grlimprclnbgr  48035  usgrexmpl2trifr  48076  gpgusgralem  48095  gpg5nbgrvtx03starlem1  48107  gpg5nbgrvtx03starlem2  48108  gpg5nbgrvtx03starlem3  48109  gpg5nbgrvtx13starlem1  48110  gpg5nbgrvtx13starlem2  48111  gpg5nbgrvtx13starlem3  48112  gpg3nbgrvtx0  48115  gpg3nbgrvtx0ALT  48116  gpg3nbgrvtx1  48117  gpg3kgrtriex  48128  gpg5edgnedg  48169  altgsumbcALT  48392  lindslinindsimp1  48497  lindszr  48509  zlmodzxznm  48537  elfzolborelfzop1  48559  blen1b  48628  reorelicc  48750  prelrrx2b  48754  inlinecirc02plem  48826  fvconst0ci  48930