Theorem olcd 875

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  pm2.48  885  pm2.49  886  orim12i  909  pm1.5  920  animorr  981  animorlr  982  cases2ALT  1049  2nreu  4384  2reu4lem  4463  n0snor2el  4776  disjord  5074  propeqop  5461  somin1  6096  nf1const  7259  soxp  8079  xpord2indlem  8097  naddcllem  8612  fowdom  9486  unxpwdom2  9503  nelaneqOLDOLD  9518  djuunxp  9845  fin1a2lem11  10332  axdc3lem2  10373  gchdomtri  10552  hargch  10596  alephgch  10597  nn1m1nn  12195  nn01to3  12891  rpneg  12976  ltpnf  13071  mnflt  13074  xrlttri  13090  xmulpnf1  13226  iccsplit  13438  elfznelfzo  13728  fvf1tp  13748  addmodlteq  13908  bc0k  14273  bcpasc  14283  hashv01gt1  14307  hashrabsn01  14335  hashsn01  14378  pr2pwpr  14441  hashtpg  14447  ccatsymb  14545  s3sndisj  14929  s3iunsndisj  14930  fsum  15682  fsumsplit  15703  fprod  15906  binomfallfaclem2  16005  fsumdvds  16277  pwp1fsum  16360  lcmfunsnlem1  16606  lcmfunsnlem2  16609  2mulprm  16662  ncoprmlnprm  16698  4sqlem17  16932  vdwlem6  16957  ram0  16993  cshwsidrepswmod0  17065  cshwsdisj  17069  basprssdmsets  17191  mreexfidimd  17616  homffval  17656  comfffval  17664  natfval  17916  xpchomfval  18145  xpccofval  18148  chnccat  18592  plusffval  18614  efmndplusg  18848  smndex1mgm  18878  sgrp2nmndlem5  18900  grpsubfval  18959  grpsubfvalALT  18960  psgnunilem1  19468  psgnunilem5  19469  gsummulg  19917  prmgrpsimpgd  20091  srgbinomlem3  20209  lringuplu  20521  scaffval  20875  drngnidl  21241  cnsubrg  21407  ipffval  21628  psrmulr  21921  pmatcoe1fsupp  22666  en2top  22950  fctop  22969  cctop  22971  metustto  24518  pcofval  24977  pmltpclem2  25416  itg1addlem5  25667  itg10a  25677  dvne0  25978  plyeq0lem  26175  plymullem1  26179  aalioulem4  26301  aalioulem5  26302  aaliou2b  26307  ang180lem3  26775  basellem2  27045  musumsum  27155  dchrhash  27234  lgsdir2lem5  27292  rpvmasumlem  27450  rpvmasum2  27475  pntlemj  27566  ltsres  27626  noetainflem4  27704  addsval  27954  mulsval  28101  mulsproplem13  28120  mulsproplem14  28121  n0s0suc  28334  n0s0m1  28354  nn1m1nns  28366  zseo  28414  halfcut  28450  bdayfinbndlem1  28459  z12zsodd  28474  tgbtwnconn1  28643  tgbtwnconn2  28644  hlid  28677  hltr  28678  hlbtwn  28679  lnhl  28683  colmid  28756  hlpasch  28824  lmieu  28852  lmiinv  28860  cgrahl  28895  cgracol  28896  inaghl  28913  edglnl  29212  umgrvad2edg  29282  nbgrnvtx0  29408  wwlksnfi  29974  clwlkclwwlklem2a  30068  clwwlknnn  30103  clwwlknon1nloop  30169  eupth2lem2  30289  frgrwopreg  30393  2wspmdisj  30407  frgrreg  30464  ex-natded5.7  30481  ex-natded5.13  30485  ex-natded9.20  30487  ex-natded9.20-2  30488  aevdemo  30530  f1ocnt  32873  linds2eq  33441  constrextdg2lem  33892  esumsnf  34208  meascnbl  34363  signsplypnf  34694  hashreprin  34764  circlemeth  34784  satfvsucsuc  35547  fmlasucdisj  35581  satfun  35593  satfv1fvfmla1  35605  2goelgoanfmla1  35606  dfrdg4  36133  outsideoftr  36311  lineunray  36329  weiunpo  36647  weiunso  36648  lindsdom  37935  ftc1anclem3  38016  dvasin  38025  areacirclem4  38032  smprngopr  38373  tsbi1  38454  tsbi2  38455  lkrshpor  39553  cdleme22b  40787  tendoex  41421  lcfrlem9  41996  aks6d1c2p2  42558  hashnexinjle  42568  grpods  42633  unitscyglem2  42635  pell1234qrdich  43289  acongtr  43406  acongrep  43408  jm2.23  43424  jm2.25  43427  fnwe2lem3  43480  kelac2lem  43492  mendplusgfval  43609  mendmulrfval  43611  onmcl  43759  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  ifpim23g  43922  frege122d  44187  clsk1indlem3  44470  refsum2cnlem1  45468  disjxp1  45500  eliuniincex  45539  eliincex  45540  fmul01lt1lem1  46014  limciccioolb  46051  sumnnodd  46060  limcicciooub  46065  wallispilem3  46495  fourierdlem35  46570  fourierdlem80  46614  fourierdlem101  46635  fourierswlem  46658  etransclem32  46694  etransclem35  46697  nnfoctbdjlem  46883  nthrucw  47316  squeezedltsq  47318  otiunsndisjX  47727  nltle2tri  47761  icceuelpartlem  47895  lighneallem3  48070  evennodd  48119  oddneven  48120  clnbgrnvtx0  48303  predgclnbgrel  48315  clnbgredg  48316  vopnbgrelself  48331  dfclnbgr6  48332  dfsclnbgr6  48334  clnbgrgrimlem  48409  clnbgrgrim  48410  grlimprclnbgr  48472  usgrexmpl2trifr  48513  gpgusgralem  48532  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg3nbgrvtx0  48552  gpg3nbgrvtx0ALT  48553  gpg3nbgrvtx1  48554  gpg3kgrtriex  48565  gpg5edgnedg  48606  altgsumbcALT  48829  lindslinindsimp1  48933  lindszr  48945  zlmodzxznm  48973  elfzolborelfzop1  48995  blen1b  49064  reorelicc  49186  prelrrx2b  49190  inlinecirc02plem  49262  fvconst0ci  49366