Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30305. (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  17587  homffval  17627  comfffval  17635  natfval  17887  xpchomfval  18116  xpccofval  18119  plusffval  18549  efmndplusg  18783  smndex1mgm  18810  sgrp2nmndlem5  18832  grpsubfval  18891  grpsubfvalALT  18892  psgnunilem1  19399  psgnunilem5  19400  gsummulg  19848  prmgrpsimpgd  20022  srgbinomlem3  20113  lringuplu  20429  scaffval  20762  drngnidl  21129  cnsubrg  21320  ipffval  21533  psrmulr  21827  pmatcoe1fsupp  22564  en2top  22848  fctop  22867  cctop  22869  metustto  24417  pcofval  24886  pmltpclem2  25326  itg1addlem5  25577  itg10a  25587  dvne0  25892  plyeq0lem  26091  plymullem1  26095  aalioulem4  26219  aalioulem5  26220  aaliou2b  26225  ang180lem3  26697  basellem2  26968  musumsum  27078  dchrhash  27158  lgsdir2lem5  27216  rpvmasumlem  27374  rpvmasum2  27399  pntlemj  27490  sltres  27550  noetainflem4  27628  addsval  27845  mulsval  27988  mulsproplem13  28007  mulsproplem14  28008  n0s0suc  28210  n0s0m1  28228  nn1m1nns  28239  zseo  28284  halfcut  28309  tgbtwnconn1  28478  tgbtwnconn2  28479  hlid  28512  hltr  28513  hlbtwn  28514  lnhl  28518  colmid  28591  hlpasch  28659  lmieu  28687  lmiinv  28695  cgrahl  28730  cgracol  28731  inaghl  28748  edglnl  29046  umgrvad2edg  29116  nbgrnvtx0  29242  wwlksnfi  29809  clwlkclwwlklem2a  29900  clwwlknnn  29935  clwwlknon1nloop  30001  eupth2lem2  30121  frgrwopreg  30225  2wspmdisj  30239  frgrreg  30296  ex-natded5.7  30313  ex-natded5.13  30317  ex-natded9.20  30319  ex-natded9.20-2  30320  aevdemo  30362  f1ocnt  32698  linds2eq  33325  constrextdg2lem  33711  esumsnf  34027  meascnbl  34182  signsplypnf  34514  hashreprin  34584  circlemeth  34604  satfvsucsuc  35325  fmlasucdisj  35359  satfun  35371  satfv1fvfmla1  35383  2goelgoanfmla1  35384  dfrdg4  35912  outsideoftr  36090  lineunray  36108  weiunpo  36426  weiunso  36427  lindsdom  37581  ftc1anclem3  37662  dvasin  37671  areacirclem4  37678  smprngopr  38019  tsbi1  38100  tsbi2  38101  lkrshpor  39073  cdleme22b  40308  tendoex  40942  lcfrlem9  41517  aks6d1c2p2  42080  hashnexinjle  42090  grpods  42155  unitscyglem2  42157  pell1234qrdich  42822  acongtr  42940  acongrep  42942  jm2.23  42958  jm2.25  42961  fnwe2lem3  43014  kelac2lem  43026  mendplusgfval  43143  mendmulrfval  43145  onmcl  43293  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  ifpim23g  43457  frege122d  43722  clsk1indlem3  44005  refsum2cnlem1  45004  disjxp1  45036  eliuniincex  45076  eliincex  45077  fmul01lt1lem1  45555  limciccioolb  45592  sumnnodd  45601  limcicciooub  45608  wallispilem3  46038  fourierdlem35  46113  fourierdlem80  46157  fourierdlem101  46178  fourierswlem  46201  etransclem32  46237  etransclem35  46240  nnfoctbdjlem  46426  squeezedltsq  46860  otiunsndisjX  47253  nltle2tri  47287  icceuelpartlem  47409  lighneallem3  47581  evennodd  47617  oddneven  47618  clnbgrnvtx0  47801  predgclnbgrel  47812  clnbgredg  47813  vopnbgrelself  47828  dfclnbgr6  47829  dfsclnbgr6  47831  clnbgrgrimlem  47906  clnbgrgrim  47907  usgrexmpl2trifr  48001  gpgusgralem  48020  gpg5nbgrvtx03starlem1  48032  gpg5nbgrvtx03starlem2  48033  gpg5nbgrvtx03starlem3  48034  gpg5nbgrvtx13starlem1  48035  gpg5nbgrvtx13starlem2  48036  gpg5nbgrvtx13starlem3  48037  gpg3nbgrvtx0  48040  gpg3nbgrvtx0ALT  48041  gpg3nbgrvtx1  48042  gpg3kgrtriex  48053  altgsumbcALT  48314  lindslinindsimp1  48419  lindszr  48431  zlmodzxznm  48459  elfzolborelfzop1  48481  blen1b  48550  reorelicc  48672  prelrrx2b  48676  inlinecirc02plem  48748  fvconst0ci  48852