Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30347. (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  4395  2reu4lem  4473  n0snor2el  4784  disjord  5081  propeqop  5450  somin1  6082  nf1const  7241  soxp  8062  xpord2indlem  8080  naddcllem  8594  fowdom  9463  unxpwdom2  9480  nelaneqOLD  9494  djuunxp  9817  fin1a2lem11  10304  axdc3lem2  10345  gchdomtri  10523  hargch  10567  alephgch  10568  nn1m1nn  12149  nn01to3  12842  rpneg  12927  ltpnf  13022  mnflt  13025  xrlttri  13041  xmulpnf1  13176  iccsplit  13388  elfznelfzo  13675  fvf1tp  13693  addmodlteq  13853  bc0k  14218  bcpasc  14228  hashv01gt1  14252  hashrabsn01  14280  hashsn01  14323  pr2pwpr  14386  hashtpg  14392  ccatsymb  14489  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  plusffval  18520  efmndplusg  18754  smndex1mgm  18781  sgrp2nmndlem5  18803  grpsubfval  18862  grpsubfvalALT  18863  psgnunilem1  19372  psgnunilem5  19373  gsummulg  19821  prmgrpsimpgd  19995  srgbinomlem3  20113  lringuplu  20429  scaffval  20783  drngnidl  21150  cnsubrg  21334  ipffval  21555  psrmulr  21849  pmatcoe1fsupp  22586  en2top  22870  fctop  22889  cctop  22891  metustto  24439  pcofval  24908  pmltpclem2  25348  itg1addlem5  25599  itg10a  25609  dvne0  25914  plyeq0lem  26113  plymullem1  26117  aalioulem4  26241  aalioulem5  26242  aaliou2b  26247  ang180lem3  26719  basellem2  26990  musumsum  27100  dchrhash  27180  lgsdir2lem5  27238  rpvmasumlem  27396  rpvmasum2  27421  pntlemj  27512  sltres  27572  noetainflem4  27650  addsval  27874  mulsval  28017  mulsproplem13  28036  mulsproplem14  28037  n0s0suc  28239  n0s0m1  28257  nn1m1nns  28268  zseo  28314  halfcut  28346  zs12zodd  28359  tgbtwnconn1  28520  tgbtwnconn2  28521  hlid  28554  hltr  28555  hlbtwn  28556  lnhl  28560  colmid  28633  hlpasch  28701  lmieu  28729  lmiinv  28737  cgrahl  28772  cgracol  28773  inaghl  28790  edglnl  29088  umgrvad2edg  29158  nbgrnvtx0  29284  wwlksnfi  29851  clwlkclwwlklem2a  29942  clwwlknnn  29977  clwwlknon1nloop  30043  eupth2lem2  30163  frgrwopreg  30267  2wspmdisj  30281  frgrreg  30338  ex-natded5.7  30355  ex-natded5.13  30359  ex-natded9.20  30361  ex-natded9.20-2  30362  aevdemo  30404  f1ocnt  32745  linds2eq  33318  constrextdg2lem  33715  esumsnf  34031  meascnbl  34186  signsplypnf  34518  hashreprin  34588  circlemeth  34608  satfvsucsuc  35338  fmlasucdisj  35372  satfun  35384  satfv1fvfmla1  35396  2goelgoanfmla1  35397  dfrdg4  35925  outsideoftr  36103  lineunray  36121  weiunpo  36439  weiunso  36440  lindsdom  37594  ftc1anclem3  37675  dvasin  37684  areacirclem4  37691  smprngopr  38032  tsbi1  38113  tsbi2  38114  lkrshpor  39086  cdleme22b  40320  tendoex  40954  lcfrlem9  41529  aks6d1c2p2  42092  hashnexinjle  42102  grpods  42167  unitscyglem2  42169  pell1234qrdich  42834  acongtr  42951  acongrep  42953  jm2.23  42969  jm2.25  42972  fnwe2lem3  43025  kelac2lem  43037  mendplusgfval  43154  mendmulrfval  43156  onmcl  43304  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  ifpim23g  43468  frege122d  43733  clsk1indlem3  44016  refsum2cnlem1  45015  disjxp1  45047  eliuniincex  45087  eliincex  45088  fmul01lt1lem1  45565  limciccioolb  45602  sumnnodd  45611  limcicciooub  45618  wallispilem3  46048  fourierdlem35  46123  fourierdlem80  46167  fourierdlem101  46188  fourierswlem  46211  etransclem32  46247  etransclem35  46250  nnfoctbdjlem  46436  squeezedltsq  46870  otiunsndisjX  47263  nltle2tri  47297  icceuelpartlem  47419  lighneallem3  47591  evennodd  47627  oddneven  47628  clnbgrnvtx0  47811  predgclnbgrel  47823  clnbgredg  47824  vopnbgrelself  47839  dfclnbgr6  47840  dfsclnbgr6  47842  clnbgrgrimlem  47917  clnbgrgrim  47918  grlimprclnbgr  47980  usgrexmpl2trifr  48021  gpgusgralem  48040  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  gpg3nbgrvtx0  48060  gpg3nbgrvtx0ALT  48061  gpg3nbgrvtx1  48062  gpg3kgrtriex  48073  gpg5edgnedg  48114  altgsumbcALT  48337  lindslinindsimp1  48442  lindszr  48454  zlmodzxznm  48482  elfzolborelfzop1  48504  blen1b  48573  reorelicc  48695  prelrrx2b  48699  inlinecirc02plem  48771  fvconst0ci  48875