Theorem olcd 871

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

Syntax hints:   → wi 4   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  pm2.48  882  pm2.49  883  orim12i  906  pm1.5  917  animorr  976  animorlr  977  cases2ALT  1044  2nreu  4349  2reu4lem  4423  n0snor2el  4724  disjord  5018  propeqop  5362  somin1  5960  nf1const  7038  soxp  7806  fowdom  9019  unxpwdom2  9036  nelaneq  9047  djuunxp  9334  fin1a2lem11  9821  axdc3lem2  9862  gchdomtri  10040  hargch  10084  alephgch  10085  nn1m1nn  11646  nn01to3  12329  rpneg  12409  ltpnf  12503  mnflt  12506  xrlttri  12520  xmulpnf1  12655  iccsplit  12863  elfznelfzo  13137  addmodlteq  13309  bc0k  13667  bcpasc  13677  hashv01gt1  13701  hashrabsn01  13730  hashsn01  13773  pr2pwpr  13833  hashtpg  13839  ccatsymb  13927  s3sndisj  14318  s3iunsndisj  14319  fsum  15069  fsumsplit  15089  fprod  15287  binomfallfaclem2  15386  fsumdvds  15650  pwp1fsum  15732  lcmfunsnlem1  15971  lcmfunsnlem2  15974  2mulprm  16027  ncoprmlnprm  16058  4sqlem17  16287  vdwlem6  16312  ram0  16348  cshwsidrepswmod0  16420  cshwsdisj  16424  basprssdmsets  16541  mreexfidimd  16913  homffval  16952  comfffval  16960  natfval  17208  xpchomfval  17421  xpccofval  17424  plusffval  17850  efmndplusg  18037  smndex1mgm  18064  sgrp2nmndlem5  18086  grpsubfval  18139  grpsubfvalALT  18140  psgnunilem1  18613  psgnunilem5  18614  gsummulg  19055  prmgrpsimpgd  19229  srgbinomlem3  19285  scaffval  19645  drngnidl  19995  cnsubrg  20151  ipffval  20337  psrmulr  20622  pmatcoe1fsupp  21306  en2top  21590  fctop  21609  cctop  21611  metustto  23160  pcofval  23615  pmltpclem2  24053  itg1addlem5  24304  itg10a  24314  dvne0  24614  plyeq0lem  24807  plymullem1  24811  aalioulem4  24931  aalioulem5  24932  aaliou2b  24937  ang180lem3  25397  basellem2  25667  musumsum  25777  dchrhash  25855  lgsdir2lem5  25913  rpvmasumlem  26071  rpvmasum2  26096  pntlemj  26187  tgbtwnconn1  26369  tgbtwnconn2  26370  hlid  26403  hltr  26404  hlbtwn  26405  lnhl  26409  colmid  26482  hlpasch  26550  lmieu  26578  lmiinv  26586  cgrahl  26621  cgracol  26622  inaghl  26639  edglnl  26936  umgrvad2edg  27003  nbgrnvtx0  27129  wwlksnfi  27692  clwlkclwwlklem2a  27783  clwwlknnn  27818  clwwlknon1nloop  27884  eupth2lem2  28004  frgrwopreg  28108  2wspmdisj  28122  frgrreg  28179  ex-natded5.7  28196  ex-natded5.13  28200  ex-natded9.20  28202  ex-natded9.20-2  28203  aevdemo  28245  f1ocnt  30551  linds2eq  30995  esumsnf  31433  meascnbl  31588  signsplypnf  31930  hashreprin  32001  circlemeth  32021  satfvsucsuc  32725  fmlasucdisj  32759  satfun  32771  satfv1fvfmla1  32783  2goelgoanfmla1  32784  sltres  33282  dfrdg4  33525  outsideoftr  33703  lineunray  33721  lindsdom  35051  ftc1anclem3  35132  dvasin  35141  areacirclem4  35148  smprngopr  35490  tsbi1  35571  tsbi2  35572  lkrshpor  36403  cdleme22b  37637  tendoex  38271  lcfrlem9  38846  pell1234qrdich  39802  acongtr  39919  acongrep  39921  jm2.23  39937  jm2.25  39940  fnwe2lem3  39996  kelac2lem  40008  mendplusgfval  40129  mendmulrfval  40131  ifpim23g  40203  frege122d  40461  clsk1indlem3  40746  refsum2cnlem1  41666  disjxp1  41703  eliuniincex  41745  eliincex  41746  fmul01lt1lem1  42226  limciccioolb  42263  sumnnodd  42272  limcicciooub  42279  wallispilem3  42709  fourierdlem35  42784  fourierdlem80  42828  fourierdlem101  42849  fourierswlem  42872  etransclem32  42908  etransclem35  42911  nnfoctbdjlem  43094  otiunsndisjX  43835  nltle2tri  43870  icceuelpartlem  43952  lighneallem3  44125  evennodd  44161  oddneven  44162  isomuspgrlem1  44345  altgsumbcALT  44755  lindslinindsimp1  44866  lindszr  44878  zlmodzxznm  44906  elfzolborelfzop1  44928  blen1b  45002  reorelicc  45124  prelrrx2b  45128  inlinecirc02plem  45200