Theorem olcd 871

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 28776. (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 206  df-or 845

This theorem is referenced by:  pm2.48  882  pm2.49  883  orim12i  906  pm1.5  917  animorr  976  animorlr  977  cases2ALT  1046  2nreu  4376  2reu4lem  4457  n0snor2el  4765  disjord  5063  propeqop  5422  somin1  6043  nf1const  7185  soxp  7979  fowdom  9339  unxpwdom2  9356  nelaneq  9367  djuunxp  9688  fin1a2lem11  10175  axdc3lem2  10216  gchdomtri  10394  hargch  10438  alephgch  10439  nn1m1nn  12003  nn01to3  12690  rpneg  12771  ltpnf  12865  mnflt  12868  xrlttri  12882  xmulpnf1  13017  iccsplit  13226  elfznelfzo  13501  addmodlteq  13675  bc0k  14034  bcpasc  14044  hashv01gt1  14068  hashrabsn01  14097  hashsn01  14140  pr2pwpr  14202  hashtpg  14208  ccatsymb  14296  s3sndisj  14687  s3iunsndisj  14688  fsum  15441  fsumsplit  15462  fprod  15660  binomfallfaclem2  15759  fsumdvds  16026  pwp1fsum  16109  lcmfunsnlem1  16351  lcmfunsnlem2  16354  2mulprm  16407  ncoprmlnprm  16441  4sqlem17  16671  vdwlem6  16696  ram0  16732  cshwsidrepswmod0  16805  cshwsdisj  16809  basprssdmsets  16934  mreexfidimd  17368  homffval  17408  comfffval  17416  natfval  17671  xpchomfval  17905  xpccofval  17908  plusffval  18341  efmndplusg  18528  smndex1mgm  18555  sgrp2nmndlem5  18577  grpsubfval  18632  grpsubfvalALT  18633  psgnunilem1  19110  psgnunilem5  19111  gsummulg  19552  prmgrpsimpgd  19726  srgbinomlem3  19787  scaffval  20150  drngnidl  20509  cnsubrg  20667  ipffval  20862  psrmulr  21162  pmatcoe1fsupp  21859  en2top  22144  fctop  22163  cctop  22165  metustto  23718  pcofval  24182  pmltpclem2  24622  itg1addlem5  24874  itg10a  24884  dvne0  25184  plyeq0lem  25380  plymullem1  25384  aalioulem4  25504  aalioulem5  25505  aaliou2b  25510  ang180lem3  25970  basellem2  26240  musumsum  26350  dchrhash  26428  lgsdir2lem5  26486  rpvmasumlem  26644  rpvmasum2  26669  pntlemj  26760  tgbtwnconn1  26945  tgbtwnconn2  26946  hlid  26979  hltr  26980  hlbtwn  26981  lnhl  26985  colmid  27058  hlpasch  27126  lmieu  27154  lmiinv  27162  cgrahl  27197  cgracol  27198  inaghl  27215  edglnl  27522  umgrvad2edg  27589  nbgrnvtx0  27715  wwlksnfi  28280  clwlkclwwlklem2a  28371  clwwlknnn  28406  clwwlknon1nloop  28472  eupth2lem2  28592  frgrwopreg  28696  2wspmdisj  28710  frgrreg  28767  ex-natded5.7  28784  ex-natded5.13  28788  ex-natded9.20  28790  ex-natded9.20-2  28791  aevdemo  28833  f1ocnt  31132  linds2eq  31584  esumsnf  32041  meascnbl  32196  signsplypnf  32538  hashreprin  32609  circlemeth  32629  satfvsucsuc  33336  fmlasucdisj  33370  satfun  33382  satfv1fvfmla1  33394  2goelgoanfmla1  33395  xpord2ind  33803  naddcllem  33840  sltres  33874  noetainflem4  33952  addsval  34135  dfrdg4  34262  outsideoftr  34440  lineunray  34458  lindsdom  35780  ftc1anclem3  35861  dvasin  35870  areacirclem4  35877  smprngopr  36219  tsbi1  36300  tsbi2  36301  lkrshpor  37128  cdleme22b  38362  tendoex  38996  lcfrlem9  39571  pell1234qrdich  40690  acongtr  40807  acongrep  40809  jm2.23  40825  jm2.25  40828  fnwe2lem3  40884  kelac2lem  40896  mendplusgfval  41017  mendmulrfval  41019  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  ifpim23g  41109  frege122d  41375  clsk1indlem3  41660  refsum2cnlem1  42587  disjxp1  42624  eliuniincex  42666  eliincex  42667  fmul01lt1lem1  43132  limciccioolb  43169  sumnnodd  43178  limcicciooub  43185  wallispilem3  43615  fourierdlem35  43690  fourierdlem80  43734  fourierdlem101  43755  fourierswlem  43778  etransclem32  43814  etransclem35  43817  nnfoctbdjlem  44000  otiunsndisjX  44782  nltle2tri  44816  icceuelpartlem  44898  lighneallem3  45070  evennodd  45106  oddneven  45107  isomuspgrlem1  45290  altgsumbcALT  45700  lindslinindsimp1  45809  lindszr  45821  zlmodzxznm  45849  elfzolborelfzop1  45871  blen1b  45945  reorelicc  46067  prelrrx2b  46071  inlinecirc02plem  46143  fvconst0ci  46197