Theorem olcd 873

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  pm2.48  883  pm2.49  884  orim12i  907  pm1.5  918  animorr  979  animorlr  980  cases2ALT  1049  2nreu  4467  2reu4lem  4545  n0snor2el  4858  disjord  5155  propeqop  5526  somin1  6165  nf1const  7340  soxp  8170  xpord2indlem  8188  naddcllem  8732  fowdom  9640  unxpwdom2  9657  nelaneq  9668  djuunxp  9990  fin1a2lem11  10479  axdc3lem2  10520  gchdomtri  10698  hargch  10742  alephgch  10743  nn1m1nn  12314  nn01to3  13006  rpneg  13089  ltpnf  13183  mnflt  13186  xrlttri  13201  xmulpnf1  13336  iccsplit  13545  elfznelfzo  13822  fvf1tp  13840  addmodlteq  13997  bc0k  14360  bcpasc  14370  hashv01gt1  14394  hashrabsn01  14422  hashsn01  14465  pr2pwpr  14528  hashtpg  14534  ccatsymb  14630  s3sndisj  15016  s3iunsndisj  15017  fsum  15768  fsumsplit  15789  fprod  15989  binomfallfaclem2  16088  fsumdvds  16356  pwp1fsum  16439  lcmfunsnlem1  16684  lcmfunsnlem2  16687  2mulprm  16740  ncoprmlnprm  16775  4sqlem17  17008  vdwlem6  17033  ram0  17069  cshwsidrepswmod0  17142  cshwsdisj  17146  basprssdmsets  17271  mreexfidimd  17708  homffval  17748  comfffval  17756  natfval  18014  xpchomfval  18248  xpccofval  18251  plusffval  18684  efmndplusg  18915  smndex1mgm  18942  sgrp2nmndlem5  18964  grpsubfval  19023  grpsubfvalALT  19024  psgnunilem1  19535  psgnunilem5  19536  gsummulg  19984  prmgrpsimpgd  20158  srgbinomlem3  20255  lringuplu  20570  scaffval  20900  drngnidl  21276  cnsubrg  21468  ipffval  21689  psrmulr  21985  pmatcoe1fsupp  22728  en2top  23013  fctop  23032  cctop  23034  metustto  24587  pcofval  25062  pmltpclem2  25503  itg1addlem5  25755  itg10a  25765  dvne0  26070  plyeq0lem  26269  plymullem1  26273  aalioulem4  26395  aalioulem5  26396  aaliou2b  26401  ang180lem3  26872  basellem2  27143  musumsum  27253  dchrhash  27333  lgsdir2lem5  27391  rpvmasumlem  27549  rpvmasum2  27574  pntlemj  27665  sltres  27725  noetainflem4  27803  addsval  28013  mulsval  28153  mulsproplem13  28172  mulsproplem14  28173  n0s0suc  28363  n0s0m1  28377  zseo  28424  halfcut  28434  tgbtwnconn1  28601  tgbtwnconn2  28602  hlid  28635  hltr  28636  hlbtwn  28637  lnhl  28641  colmid  28714  hlpasch  28782  lmieu  28810  lmiinv  28818  cgrahl  28853  cgracol  28854  inaghl  28871  edglnl  29178  umgrvad2edg  29248  nbgrnvtx0  29374  wwlksnfi  29939  clwlkclwwlklem2a  30030  clwwlknnn  30065  clwwlknon1nloop  30131  eupth2lem2  30251  frgrwopreg  30355  2wspmdisj  30369  frgrreg  30426  ex-natded5.7  30443  ex-natded5.13  30447  ex-natded9.20  30449  ex-natded9.20-2  30450  aevdemo  30492  f1ocnt  32807  linds2eq  33374  esumsnf  34028  meascnbl  34183  signsplypnf  34527  hashreprin  34597  circlemeth  34617  satfvsucsuc  35333  fmlasucdisj  35367  satfun  35379  satfv1fvfmla1  35391  2goelgoanfmla1  35392  dfrdg4  35915  outsideoftr  36093  lineunray  36111  weiunpo  36431  weiunso  36432  lindsdom  37574  ftc1anclem3  37655  dvasin  37664  areacirclem4  37671  smprngopr  38012  tsbi1  38093  tsbi2  38094  lkrshpor  39063  cdleme22b  40298  tendoex  40932  lcfrlem9  41507  aks6d1c2p2  42076  hashnexinjle  42086  grpods  42151  unitscyglem2  42153  pell1234qrdich  42817  acongtr  42935  acongrep  42937  jm2.23  42953  jm2.25  42956  fnwe2lem3  43009  kelac2lem  43021  mendplusgfval  43142  mendmulrfval  43144  onmcl  43293  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  ifpim23g  43457  frege122d  43722  clsk1indlem3  44005  refsum2cnlem1  44937  disjxp1  44971  eliuniincex  45011  eliincex  45012  fmul01lt1lem1  45505  limciccioolb  45542  sumnnodd  45551  limcicciooub  45558  wallispilem3  45988  fourierdlem35  46063  fourierdlem80  46107  fourierdlem101  46128  fourierswlem  46151  etransclem32  46187  etransclem35  46190  nnfoctbdjlem  46376  otiunsndisjX  47194  nltle2tri  47228  icceuelpartlem  47309  lighneallem3  47481  evennodd  47517  oddneven  47518  clnbgrnvtx0  47700  predgclnbgrel  47711  clnbgredg  47712  vopnbgrelself  47727  dfclnbgr6  47728  dfsclnbgr6  47730  clnbgrgrimlem  47785  clnbgrgrim  47786  usgrexmpl2trifr  47852  altgsumbcALT  48078  lindslinindsimp1  48186  lindszr  48198  zlmodzxznm  48226  elfzolborelfzop1  48248  blen1b  48322  reorelicc  48444  prelrrx2b  48448  inlinecirc02plem  48520  fvconst0ci  48572