Theorem olcd 871

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30128. (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  881  pm2.49  882  orim12i  905  pm1.5  916  animorr  975  animorlr  976  cases2ALT  1045  2nreu  4434  2reu4lem  4518  n0snor2el  4827  disjord  5127  propeqop  5498  somin1  6125  nf1const  7295  soxp  8110  xpord2indlem  8128  naddcllem  8672  fowdom  9563  unxpwdom2  9580  nelaneq  9591  djuunxp  9913  fin1a2lem11  10402  axdc3lem2  10443  gchdomtri  10621  hargch  10665  alephgch  10666  nn1m1nn  12231  nn01to3  12923  rpneg  13004  ltpnf  13098  mnflt  13101  xrlttri  13116  xmulpnf1  13251  iccsplit  13460  elfznelfzo  13735  addmodlteq  13909  bc0k  14269  bcpasc  14279  hashv01gt1  14303  hashrabsn01  14331  hashsn01  14374  pr2pwpr  14438  hashtpg  14444  ccatsymb  14530  s3sndisj  14912  s3iunsndisj  14913  fsum  15664  fsumsplit  15685  fprod  15883  binomfallfaclem2  15982  fsumdvds  16250  pwp1fsum  16333  lcmfunsnlem1  16573  lcmfunsnlem2  16576  2mulprm  16629  ncoprmlnprm  16665  4sqlem17  16895  vdwlem6  16920  ram0  16956  cshwsidrepswmod0  17029  cshwsdisj  17033  basprssdmsets  17158  mreexfidimd  17595  homffval  17635  comfffval  17643  natfval  17901  xpchomfval  18135  xpccofval  18138  plusffval  18571  efmndplusg  18797  smndex1mgm  18824  sgrp2nmndlem5  18846  grpsubfval  18905  grpsubfvalALT  18906  psgnunilem1  19405  psgnunilem5  19406  gsummulg  19854  prmgrpsimpgd  20028  srgbinomlem3  20125  lringuplu  20436  scaffval  20718  drngnidl  21093  cnsubrg  21291  ipffval  21511  psrmulr  21815  pmatcoe1fsupp  22527  en2top  22812  fctop  22831  cctop  22833  metustto  24386  pcofval  24861  pmltpclem2  25302  itg1addlem5  25554  itg10a  25564  dvne0  25868  plyeq0lem  26066  plymullem1  26070  aalioulem4  26191  aalioulem5  26192  aaliou2b  26197  ang180lem3  26662  basellem2  26933  musumsum  27043  dchrhash  27123  lgsdir2lem5  27181  rpvmasumlem  27339  rpvmasum2  27364  pntlemj  27455  sltres  27514  noetainflem4  27592  addsval  27798  mulsval  27928  mulsproplem13  27947  mulsproplem14  27948  tgbtwnconn1  28298  tgbtwnconn2  28299  hlid  28332  hltr  28333  hlbtwn  28334  lnhl  28338  colmid  28411  hlpasch  28479  lmieu  28507  lmiinv  28515  cgrahl  28550  cgracol  28551  inaghl  28568  edglnl  28875  umgrvad2edg  28942  nbgrnvtx0  29068  wwlksnfi  29632  clwlkclwwlklem2a  29723  clwwlknnn  29758  clwwlknon1nloop  29824  eupth2lem2  29944  frgrwopreg  30048  2wspmdisj  30062  frgrreg  30119  ex-natded5.7  30136  ex-natded5.13  30140  ex-natded9.20  30142  ex-natded9.20-2  30143  aevdemo  30185  f1ocnt  32485  linds2eq  32969  esumsnf  33554  meascnbl  33709  signsplypnf  34053  hashreprin  34123  circlemeth  34143  satfvsucsuc  34847  fmlasucdisj  34881  satfun  34893  satfv1fvfmla1  34905  2goelgoanfmla1  34906  dfrdg4  35419  outsideoftr  35597  lineunray  35615  lindsdom  36976  ftc1anclem3  37057  dvasin  37066  areacirclem4  37073  smprngopr  37414  tsbi1  37495  tsbi2  37496  lkrshpor  38471  cdleme22b  39706  tendoex  40340  lcfrlem9  40915  aks6d1c2p2  41454  pell1234qrdich  42113  acongtr  42231  acongrep  42233  jm2.23  42249  jm2.25  42252  fnwe2lem3  42308  kelac2lem  42320  mendplusgfval  42441  mendmulrfval  42443  onmcl  42595  fzunt  42720  fzuntd  42721  fzunt1d  42722  fzuntgd  42723  ifpim23g  42760  frege122d  43025  clsk1indlem3  43308  refsum2cnlem1  44235  disjxp1  44269  eliuniincex  44311  eliincex  44312  fmul01lt1lem1  44810  limciccioolb  44847  sumnnodd  44856  limcicciooub  44863  wallispilem3  45293  fourierdlem35  45368  fourierdlem80  45412  fourierdlem101  45433  fourierswlem  45456  etransclem32  45492  etransclem35  45495  nnfoctbdjlem  45681  otiunsndisjX  46497  nltle2tri  46531  icceuelpartlem  46613  lighneallem3  46785  evennodd  46821  oddneven  46822  isomuspgrlem1  47005  altgsumbcALT  47243  lindslinindsimp1  47351  lindszr  47363  zlmodzxznm  47391  elfzolborelfzop1  47413  blen1b  47487  reorelicc  47609  prelrrx2b  47613  inlinecirc02plem  47685  fvconst0ci  47737