Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30382. (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  4403  2reu4lem  4481  n0snor2el  4793  disjord  5091  propeqop  5462  somin1  6094  nf1const  7261  soxp  8085  xpord2indlem  8103  naddcllem  8617  fowdom  9500  unxpwdom2  9517  nelaneq  9528  djuunxp  9850  fin1a2lem11  10339  axdc3lem2  10380  gchdomtri  10558  hargch  10602  alephgch  10603  nn1m1nn  12183  nn01to3  12876  rpneg  12961  ltpnf  13056  mnflt  13059  xrlttri  13075  xmulpnf1  13210  iccsplit  13422  elfznelfzo  13709  fvf1tp  13727  addmodlteq  13887  bc0k  14252  bcpasc  14262  hashv01gt1  14286  hashrabsn01  14314  hashsn01  14357  pr2pwpr  14420  hashtpg  14426  ccatsymb  14523  s3sndisj  14909  s3iunsndisj  14910  fsum  15662  fsumsplit  15683  fprod  15883  binomfallfaclem2  15982  fsumdvds  16254  pwp1fsum  16337  lcmfunsnlem1  16583  lcmfunsnlem2  16586  2mulprm  16639  ncoprmlnprm  16674  4sqlem17  16908  vdwlem6  16933  ram0  16969  cshwsidrepswmod0  17041  cshwsdisj  17045  basprssdmsets  17167  mreexfidimd  17591  homffval  17631  comfffval  17639  natfval  17891  xpchomfval  18120  xpccofval  18123  plusffval  18555  efmndplusg  18789  smndex1mgm  18816  sgrp2nmndlem5  18838  grpsubfval  18897  grpsubfvalALT  18898  psgnunilem1  19407  psgnunilem5  19408  gsummulg  19856  prmgrpsimpgd  20030  srgbinomlem3  20148  lringuplu  20464  scaffval  20818  drngnidl  21185  cnsubrg  21369  ipffval  21590  psrmulr  21884  pmatcoe1fsupp  22621  en2top  22905  fctop  22924  cctop  22926  metustto  24474  pcofval  24943  pmltpclem2  25383  itg1addlem5  25634  itg10a  25644  dvne0  25949  plyeq0lem  26148  plymullem1  26152  aalioulem4  26276  aalioulem5  26277  aaliou2b  26282  ang180lem3  26754  basellem2  27025  musumsum  27135  dchrhash  27215  lgsdir2lem5  27273  rpvmasumlem  27431  rpvmasum2  27456  pntlemj  27547  sltres  27607  noetainflem4  27685  addsval  27909  mulsval  28052  mulsproplem13  28071  mulsproplem14  28072  n0s0suc  28274  n0s0m1  28292  nn1m1nns  28303  zseo  28349  halfcut  28381  zs12zodd  28394  tgbtwnconn1  28555  tgbtwnconn2  28556  hlid  28589  hltr  28590  hlbtwn  28591  lnhl  28595  colmid  28668  hlpasch  28736  lmieu  28764  lmiinv  28772  cgrahl  28807  cgracol  28808  inaghl  28825  edglnl  29123  umgrvad2edg  29193  nbgrnvtx0  29319  wwlksnfi  29886  clwlkclwwlklem2a  29977  clwwlknnn  30012  clwwlknon1nloop  30078  eupth2lem2  30198  frgrwopreg  30302  2wspmdisj  30316  frgrreg  30373  ex-natded5.7  30390  ex-natded5.13  30394  ex-natded9.20  30396  ex-natded9.20-2  30397  aevdemo  30439  f1ocnt  32775  linds2eq  33345  constrextdg2lem  33731  esumsnf  34047  meascnbl  34202  signsplypnf  34534  hashreprin  34604  circlemeth  34624  satfvsucsuc  35345  fmlasucdisj  35379  satfun  35391  satfv1fvfmla1  35403  2goelgoanfmla1  35404  dfrdg4  35932  outsideoftr  36110  lineunray  36128  weiunpo  36446  weiunso  36447  lindsdom  37601  ftc1anclem3  37682  dvasin  37691  areacirclem4  37698  smprngopr  38039  tsbi1  38120  tsbi2  38121  lkrshpor  39093  cdleme22b  40328  tendoex  40962  lcfrlem9  41537  aks6d1c2p2  42100  hashnexinjle  42110  grpods  42175  unitscyglem2  42177  pell1234qrdich  42842  acongtr  42960  acongrep  42962  jm2.23  42978  jm2.25  42981  fnwe2lem3  43034  kelac2lem  43046  mendplusgfval  43163  mendmulrfval  43165  onmcl  43313  fzunt  43437  fzuntd  43438  fzunt1d  43439  fzuntgd  43440  ifpim23g  43477  frege122d  43742  clsk1indlem3  44025  refsum2cnlem1  45024  disjxp1  45056  eliuniincex  45096  eliincex  45097  fmul01lt1lem1  45575  limciccioolb  45612  sumnnodd  45621  limcicciooub  45628  wallispilem3  46058  fourierdlem35  46133  fourierdlem80  46177  fourierdlem101  46198  fourierswlem  46221  etransclem32  46257  etransclem35  46260  nnfoctbdjlem  46446  squeezedltsq  46880  otiunsndisjX  47273  nltle2tri  47307  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  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  gpg3nbgrvtx0  48060  gpg3nbgrvtx0ALT  48061  gpg3nbgrvtx1  48062  gpg3kgrtriex  48073  altgsumbcALT  48334  lindslinindsimp1  48439  lindszr  48451  zlmodzxznm  48479  elfzolborelfzop1  48501  blen1b  48570  reorelicc  48692  prelrrx2b  48696  inlinecirc02plem  48768  fvconst0ci  48872