Theorem olcd 870

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

Syntax hints:   → wi 4   ∨ wo 843

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 844

This theorem is referenced by:  pm2.48  881  pm2.49  882  orim12i  905  pm1.5  916  animorr  975  animorlr  976  cases2ALT  1045  2nreu  4372  2reu4lem  4453  n0snor2el  4761  disjord  5058  propeqop  5415  somin1  6027  nf1const  7156  soxp  7941  fowdom  9260  unxpwdom2  9277  nelaneq  9288  djuunxp  9610  fin1a2lem11  10097  axdc3lem2  10138  gchdomtri  10316  hargch  10360  alephgch  10361  nn1m1nn  11924  nn01to3  12610  rpneg  12691  ltpnf  12785  mnflt  12788  xrlttri  12802  xmulpnf1  12937  iccsplit  13146  elfznelfzo  13420  addmodlteq  13594  bc0k  13953  bcpasc  13963  hashv01gt1  13987  hashrabsn01  14016  hashsn01  14059  pr2pwpr  14121  hashtpg  14127  ccatsymb  14215  s3sndisj  14606  s3iunsndisj  14607  fsum  15360  fsumsplit  15381  fprod  15579  binomfallfaclem2  15678  fsumdvds  15945  pwp1fsum  16028  lcmfunsnlem1  16270  lcmfunsnlem2  16273  2mulprm  16326  ncoprmlnprm  16360  4sqlem17  16590  vdwlem6  16615  ram0  16651  cshwsidrepswmod0  16724  cshwsdisj  16728  basprssdmsets  16853  mreexfidimd  17276  homffval  17316  comfffval  17324  natfval  17578  xpchomfval  17812  xpccofval  17815  plusffval  18247  efmndplusg  18434  smndex1mgm  18461  sgrp2nmndlem5  18483  grpsubfval  18538  grpsubfvalALT  18539  psgnunilem1  19016  psgnunilem5  19017  gsummulg  19458  prmgrpsimpgd  19632  srgbinomlem3  19693  scaffval  20056  drngnidl  20413  cnsubrg  20570  ipffval  20765  psrmulr  21063  pmatcoe1fsupp  21758  en2top  22043  fctop  22062  cctop  22064  metustto  23615  pcofval  24079  pmltpclem2  24518  itg1addlem5  24770  itg10a  24780  dvne0  25080  plyeq0lem  25276  plymullem1  25280  aalioulem4  25400  aalioulem5  25401  aaliou2b  25406  ang180lem3  25866  basellem2  26136  musumsum  26246  dchrhash  26324  lgsdir2lem5  26382  rpvmasumlem  26540  rpvmasum2  26565  pntlemj  26656  tgbtwnconn1  26840  tgbtwnconn2  26841  hlid  26874  hltr  26875  hlbtwn  26876  lnhl  26880  colmid  26953  hlpasch  27021  lmieu  27049  lmiinv  27057  cgrahl  27092  cgracol  27093  inaghl  27110  edglnl  27416  umgrvad2edg  27483  nbgrnvtx0  27609  wwlksnfi  28172  clwlkclwwlklem2a  28263  clwwlknnn  28298  clwwlknon1nloop  28364  eupth2lem2  28484  frgrwopreg  28588  2wspmdisj  28602  frgrreg  28659  ex-natded5.7  28676  ex-natded5.13  28680  ex-natded9.20  28682  ex-natded9.20-2  28683  aevdemo  28725  f1ocnt  31025  linds2eq  31477  esumsnf  31932  meascnbl  32087  signsplypnf  32429  hashreprin  32500  circlemeth  32520  satfvsucsuc  33227  fmlasucdisj  33261  satfun  33273  satfv1fvfmla1  33285  2goelgoanfmla1  33286  xpord2ind  33721  naddcllem  33758  sltres  33792  noetainflem4  33870  addsval  34053  dfrdg4  34180  outsideoftr  34358  lineunray  34376  lindsdom  35698  ftc1anclem3  35779  dvasin  35788  areacirclem4  35795  smprngopr  36137  tsbi1  36218  tsbi2  36219  lkrshpor  37048  cdleme22b  38282  tendoex  38916  lcfrlem9  39491  pell1234qrdich  40599  acongtr  40716  acongrep  40718  jm2.23  40734  jm2.25  40737  fnwe2lem3  40793  kelac2lem  40805  mendplusgfval  40926  mendmulrfval  40928  ifpim23g  41000  frege122d  41257  clsk1indlem3  41542  refsum2cnlem1  42469  disjxp1  42506  eliuniincex  42548  eliincex  42549  fmul01lt1lem1  43015  limciccioolb  43052  sumnnodd  43061  limcicciooub  43068  wallispilem3  43498  fourierdlem35  43573  fourierdlem80  43617  fourierdlem101  43638  fourierswlem  43661  etransclem32  43697  etransclem35  43700  nnfoctbdjlem  43883  otiunsndisjX  44658  nltle2tri  44693  icceuelpartlem  44775  lighneallem3  44947  evennodd  44983  oddneven  44984  isomuspgrlem1  45167  altgsumbcALT  45577  lindslinindsimp1  45686  lindszr  45698  zlmodzxznm  45726  elfzolborelfzop1  45748  blen1b  45822  reorelicc  45944  prelrrx2b  45948  inlinecirc02plem  46020  fvconst0ci  46074