Theorem olcd 872

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

Syntax hints:   → wi 4   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  pm2.48  883  pm2.49  884  orim12i  907  pm1.5  918  animorr  977  animorlr  978  cases2ALT  1047  2nreu  4406  2reu4lem  4488  n0snor2el  4796  disjord  5098  propeqop  5469  somin1  6092  nf1const  7255  soxp  8066  xpord2indlem  8084  naddcllem  8627  fowdom  9516  unxpwdom2  9533  nelaneq  9544  djuunxp  9866  fin1a2lem11  10355  axdc3lem2  10396  gchdomtri  10574  hargch  10618  alephgch  10619  nn1m1nn  12183  nn01to3  12875  rpneg  12956  ltpnf  13050  mnflt  13053  xrlttri  13068  xmulpnf1  13203  iccsplit  13412  elfznelfzo  13687  addmodlteq  13861  bc0k  14221  bcpasc  14231  hashv01gt1  14255  hashrabsn01  14283  hashsn01  14326  pr2pwpr  14390  hashtpg  14396  ccatsymb  14482  s3sndisj  14864  s3iunsndisj  14865  fsum  15616  fsumsplit  15637  fprod  15835  binomfallfaclem2  15934  fsumdvds  16201  pwp1fsum  16284  lcmfunsnlem1  16524  lcmfunsnlem2  16527  2mulprm  16580  ncoprmlnprm  16614  4sqlem17  16844  vdwlem6  16869  ram0  16905  cshwsidrepswmod0  16978  cshwsdisj  16982  basprssdmsets  17107  mreexfidimd  17544  homffval  17584  comfffval  17592  natfval  17847  xpchomfval  18081  xpccofval  18084  plusffval  18517  efmndplusg  18704  smndex1mgm  18731  sgrp2nmndlem5  18753  grpsubfval  18808  grpsubfvalALT  18809  psgnunilem1  19289  psgnunilem5  19290  gsummulg  19733  prmgrpsimpgd  19907  srgbinomlem3  19973  lringuplu  20224  scaffval  20397  drngnidl  20758  cnsubrg  20894  ipffval  21089  psrmulr  21389  pmatcoe1fsupp  22087  en2top  22372  fctop  22391  cctop  22393  metustto  23946  pcofval  24410  pmltpclem2  24850  itg1addlem5  25102  itg10a  25112  dvne0  25412  plyeq0lem  25608  plymullem1  25612  aalioulem4  25732  aalioulem5  25733  aaliou2b  25738  ang180lem3  26198  basellem2  26468  musumsum  26578  dchrhash  26656  lgsdir2lem5  26714  rpvmasumlem  26872  rpvmasum2  26897  pntlemj  26988  sltres  27047  noetainflem4  27125  addsval  27317  mulsval  27417  tgbtwnconn1  27580  tgbtwnconn2  27581  hlid  27614  hltr  27615  hlbtwn  27616  lnhl  27620  colmid  27693  hlpasch  27761  lmieu  27789  lmiinv  27797  cgrahl  27832  cgracol  27833  inaghl  27850  edglnl  28157  umgrvad2edg  28224  nbgrnvtx0  28350  wwlksnfi  28914  clwlkclwwlklem2a  29005  clwwlknnn  29040  clwwlknon1nloop  29106  eupth2lem2  29226  frgrwopreg  29330  2wspmdisj  29344  frgrreg  29401  ex-natded5.7  29418  ex-natded5.13  29422  ex-natded9.20  29424  ex-natded9.20-2  29425  aevdemo  29467  f1ocnt  31773  linds2eq  32241  esumsnf  32752  meascnbl  32907  signsplypnf  33251  hashreprin  33322  circlemeth  33342  satfvsucsuc  34046  fmlasucdisj  34080  satfun  34092  satfv1fvfmla1  34104  2goelgoanfmla1  34105  dfrdg4  34612  outsideoftr  34790  lineunray  34808  lindsdom  36145  ftc1anclem3  36226  dvasin  36235  areacirclem4  36242  smprngopr  36584  tsbi1  36665  tsbi2  36666  lkrshpor  37642  cdleme22b  38877  tendoex  39511  lcfrlem9  40086  aks6d1c2p2  40622  pell1234qrdich  41242  acongtr  41360  acongrep  41362  jm2.23  41378  jm2.25  41381  fnwe2lem3  41437  kelac2lem  41449  mendplusgfval  41570  mendmulrfval  41572  onmcl  41724  fzunt  41849  fzuntd  41850  fzunt1d  41851  fzuntgd  41852  ifpim23g  41889  frege122d  42154  clsk1indlem3  42437  refsum2cnlem1  43364  disjxp1  43399  eliuniincex  43441  eliincex  43442  fmul01lt1lem1  43945  limciccioolb  43982  sumnnodd  43991  limcicciooub  43998  wallispilem3  44428  fourierdlem35  44503  fourierdlem80  44547  fourierdlem101  44568  fourierswlem  44591  etransclem32  44627  etransclem35  44630  nnfoctbdjlem  44816  otiunsndisjX  45631  nltle2tri  45665  icceuelpartlem  45747  lighneallem3  45919  evennodd  45955  oddneven  45956  isomuspgrlem1  46139  altgsumbcALT  46549  lindslinindsimp1  46658  lindszr  46670  zlmodzxznm  46698  elfzolborelfzop1  46720  blen1b  46794  reorelicc  46916  prelrrx2b  46920  inlinecirc02plem  46992  fvconst0ci  47045