Theorem olcd 874

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  pm2.48  884  pm2.49  885  orim12i  908  pm1.5  919  animorr  980  animorlr  981  cases2ALT  1048  2nreu  4393  2reu4lem  4471  n0snor2el  4784  disjord  5082  propeqop  5450  somin1  6085  nf1const  7244  soxp  8065  xpord2indlem  8083  naddcllem  8597  fowdom  9463  unxpwdom2  9480  nelaneqOLD  9494  djuunxp  9820  fin1a2lem11  10307  axdc3lem2  10348  gchdomtri  10526  hargch  10570  alephgch  10571  nn1m1nn  12152  nn01to3  12845  rpneg  12930  ltpnf  13025  mnflt  13028  xrlttri  13044  xmulpnf1  13179  iccsplit  13391  elfznelfzo  13679  fvf1tp  13699  addmodlteq  13859  bc0k  14224  bcpasc  14234  hashv01gt1  14258  hashrabsn01  14286  hashsn01  14329  pr2pwpr  14392  hashtpg  14398  ccatsymb  14496  s3sndisj  14880  s3iunsndisj  14881  fsum  15633  fsumsplit  15654  fprod  15854  binomfallfaclem2  15953  fsumdvds  16225  pwp1fsum  16308  lcmfunsnlem1  16554  lcmfunsnlem2  16557  2mulprm  16610  ncoprmlnprm  16645  4sqlem17  16879  vdwlem6  16904  ram0  16940  cshwsidrepswmod0  17012  cshwsdisj  17016  basprssdmsets  17138  mreexfidimd  17562  homffval  17602  comfffval  17610  natfval  17862  xpchomfval  18091  xpccofval  18094  chnccat  18538  plusffval  18560  efmndplusg  18794  smndex1mgm  18821  sgrp2nmndlem5  18843  grpsubfval  18902  grpsubfvalALT  18903  psgnunilem1  19411  psgnunilem5  19412  gsummulg  19860  prmgrpsimpgd  20034  srgbinomlem3  20152  lringuplu  20465  scaffval  20819  drngnidl  21186  cnsubrg  21370  ipffval  21591  psrmulr  21885  pmatcoe1fsupp  22622  en2top  22906  fctop  22925  cctop  22927  metustto  24474  pcofval  24943  pmltpclem2  25383  itg1addlem5  25634  itg10a  25644  dvne0  25949  plyeq0lem  26148  plymullem1  26152  aalioulem4  26276  aalioulem5  26277  aaliou2b  26282  ang180lem3  26754  basellem2  27025  musumsum  27135  dchrhash  27215  lgsdir2lem5  27273  rpvmasumlem  27431  rpvmasum2  27456  pntlemj  27547  sltres  27607  noetainflem4  27685  addsval  27911  mulsval  28054  mulsproplem13  28073  mulsproplem14  28074  n0s0suc  28276  n0s0m1  28294  nn1m1nns  28305  zseo  28351  halfcut  28384  zs12zodd  28398  tgbtwnconn1  28559  tgbtwnconn2  28560  hlid  28593  hltr  28594  hlbtwn  28595  lnhl  28599  colmid  28672  hlpasch  28740  lmieu  28768  lmiinv  28776  cgrahl  28811  cgracol  28812  inaghl  28829  edglnl  29128  umgrvad2edg  29198  nbgrnvtx0  29324  wwlksnfi  29891  clwlkclwwlklem2a  29985  clwwlknnn  30020  clwwlknon1nloop  30086  eupth2lem2  30206  frgrwopreg  30310  2wspmdisj  30324  frgrreg  30381  ex-natded5.7  30398  ex-natded5.13  30402  ex-natded9.20  30404  ex-natded9.20-2  30405  aevdemo  30447  f1ocnt  32789  linds2eq  33353  constrextdg2lem  33768  esumsnf  34084  meascnbl  34239  signsplypnf  34570  hashreprin  34640  circlemeth  34660  satfvsucsuc  35416  fmlasucdisj  35450  satfun  35462  satfv1fvfmla1  35474  2goelgoanfmla1  35475  dfrdg4  36002  outsideoftr  36180  lineunray  36198  weiunpo  36516  weiunso  36517  lindsdom  37660  ftc1anclem3  37741  dvasin  37750  areacirclem4  37757  smprngopr  38098  tsbi1  38179  tsbi2  38180  lkrshpor  39212  cdleme22b  40446  tendoex  41080  lcfrlem9  41655  aks6d1c2p2  42218  hashnexinjle  42228  grpods  42293  unitscyglem2  42295  pell1234qrdich  42959  acongtr  43076  acongrep  43078  jm2.23  43094  jm2.25  43097  fnwe2lem3  43150  kelac2lem  43162  mendplusgfval  43279  mendmulrfval  43281  onmcl  43429  fzunt  43553  fzuntd  43554  fzunt1d  43555  fzuntgd  43556  ifpim23g  43593  frege122d  43858  clsk1indlem3  44141  refsum2cnlem1  45139  disjxp1  45171  eliuniincex  45211  eliincex  45212  fmul01lt1lem1  45689  limciccioolb  45726  sumnnodd  45735  limcicciooub  45740  wallispilem3  46170  fourierdlem35  46245  fourierdlem80  46289  fourierdlem101  46310  fourierswlem  46333  etransclem32  46369  etransclem35  46372  nnfoctbdjlem  46558  nthrucw  46989  squeezedltsq  46991  otiunsndisjX  47384  nltle2tri  47418  icceuelpartlem  47540  lighneallem3  47712  evennodd  47748  oddneven  47749  clnbgrnvtx0  47932  predgclnbgrel  47944  clnbgredg  47945  vopnbgrelself  47960  dfclnbgr6  47961  dfsclnbgr6  47963  clnbgrgrimlem  48038  clnbgrgrim  48039  grlimprclnbgr  48101  usgrexmpl2trifr  48142  gpgusgralem  48161  gpg5nbgrvtx03starlem1  48173  gpg5nbgrvtx03starlem2  48174  gpg5nbgrvtx03starlem3  48175  gpg5nbgrvtx13starlem1  48176  gpg5nbgrvtx13starlem2  48177  gpg5nbgrvtx13starlem3  48178  gpg3nbgrvtx0  48181  gpg3nbgrvtx0ALT  48182  gpg3nbgrvtx1  48183  gpg3kgrtriex  48194  gpg5edgnedg  48235  altgsumbcALT  48458  lindslinindsimp1  48563  lindszr  48575  zlmodzxznm  48603  elfzolborelfzop1  48625  blen1b  48694  reorelicc  48816  prelrrx2b  48820  inlinecirc02plem  48892  fvconst0ci  48996