Theorem olcd 887

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

Syntax hints:   → wi 4   ∨ wo 860

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 861

This theorem is referenced by:  pm2.48  897  pm2.49  898  orim12i  921  pm1.5  932  animorr  994  animorlr  995  cases2ALT  1064  2nreu  4409  2reu4lem  4484  n0snor2el  4798  disjord  5098  propeqop  5490  somin1  6133  nf1const  7302  soxp  8121  xpord2indlem  8139  naddcllem  8658  fowdom  9529  unxpwdom2  9546  nelaneqOLDOLD  9562  djuunxp  9903  fin1a2lem11  10389  axdc3lem2  10430  gchdomtri  10609  hargch  10653  alephgch  10654  nn1m1nn  12249  nn01to3  12960  rpneg  13045  ltpnf  13140  mnflt  13143  xrlttri  13159  xmulpnf1  13295  iccsplit  13507  elfznelfzo  13798  fvf1tp  13818  addmodlteq  13978  bc0k  14343  bcpasc  14353  hashv01gt1  14377  hashrabsn01  14405  hashsn01  14449  pr2pwpr  14512  hashtpg  14518  ccatsymb  14616  s3sndisj  15000  s3iunsndisj  15001  fsum  15767  fsumsplit  15788  fprod  15991  binomfallfaclem2  16089  fsumdvds  16361  pwp1fsum  16444  lcmfunsnlem1  16690  lcmfunsnlem2  16693  2mulprm  16746  ncoprmlnprm  16782  4sqlem17  17016  vdwlem6  17041  ram0  17077  cshwsidrepswmod0  17149  cshwsdisj  17153  basprssdmsets  17276  mreexfidimd  17701  homffval  17741  comfffval  17749  natfval  18001  xpchomfval  18230  xpccofval  18233  chnccat  18677  plusffval  18699  efmndplusg  18934  smndex1mgm  18964  sgrp2nmndlem5  18986  grpsubfval  19045  grpsubfvalALT  19046  psgnunilem1  19558  psgnunilem5  19559  gsummulg  20007  prmgrpsimpgd  20181  srgbinomlem3  20305  lringuplu  20643  scaffval  21001  drngnidl  21377  cnsubrg  21577  ipffval  21798  psrmulr  22092  pmatcoe1fsupp  22858  en2top  23142  fctop  23161  cctop  23163  metustto  24710  pcofval  25169  pmltpclem2  25608  itg1addlem5  25859  itg10a  25869  dvne0  26170  plyeq0lem  26367  plymullem1  26371  aalioulem4  26498  aalioulem5  26499  aaliou2b  26504  ang180lem3  26976  basellem2  27246  musumsum  27356  dchrhash  27435  lgsdir2lem5  27493  rpvmasumlem  27651  rpvmasum2  27676  pntlemj  27767  ltsres  27826  noetainflem4  27904  addsval  28155  mulsval  28302  mulsproplem13  28321  mulsproplem14  28322  n0s0suc  28535  n0s0m1  28555  nn1m1nns  28567  zseo  28615  halfcut  28651  bdayfinbndlem1  28660  z12zsodd  28675  tgbtwnconn1  28844  tgbtwnconn2  28845  hlid  28881  hltr  28882  hlbtwn  28883  lnhl  28887  colmid  28965  hlpasch  29038  lnincplng  29066  lmieu  29093  lmiinv  29101  cgrahl  29138  cgracol  29139  inaghl  29162  prlngd  29189  edglnl  29493  umgrvad2edg  29563  nbgrnvtx0  29689  wwlksnfi  30255  clwlkclwwlklem2a  30349  clwwlknnn  30384  clwwlknon1nloop  30450  eupth2lem2  30570  frgrwopreg  30674  2wspmdisj  30688  frgrreg  30745  ex-natded5.7  30762  ex-natded5.13  30766  ex-natded9.20  30768  ex-natded9.20-2  30769  aevdemo  30811  f1ocnt  33145  linds2eq  33694  constrextdg2lem  34138  esumsnf  34454  meascnbl  34609  signsplypnf  34937  hashreprin  35007  circlemeth  35027  satfvsucsuc  35857  fmlasucdisj  35891  satfun  35903  satfv1fvfmla1  35915  2goelgoanfmla1  35916  dfrdg4  36443  outsideoftr  36621  lineunray  36639  weiunpo  36976  weiunso  36977  lindsdom  38265  ftc1anclem3  38346  dvasin  38355  areacirclem4  38362  smprngopr  38703  tsbi1  38782  tsbi2  38783  lkrshpor  39881  cdleme22b  41115  tendoex  41749  lcfrlem9  42324  aks6d1c2p2  42886  hashnexinjle  42896  grpods  42961  unitscyglem2  42963  pell1234qrdich  43588  acongtr  43705  acongrep  43707  jm2.23  43723  jm2.25  43726  fnwe2lem3  43779  kelac2lem  43791  mendplusgfval  43908  mendmulrfval  43910  onmcl  44058  fzunt  44181  fzuntd  44182  fzunt1d  44183  fzuntgd  44184  ifpim23g  44221  frege122d  44486  clsk1indlem3  44769  refsum2cnlem1  45757  disjxp1  45789  eliuniincex  45827  eliincex  45828  fmul01lt1lem1  46300  limciccioolb  46337  sumnnodd  46346  limcicciooub  46351  wallispilem3  46781  fourierdlem35  46856  fourierdlem80  46900  fourierdlem101  46921  fourierswlem  46944  etransclem32  46980  etransclem35  46983  nnfoctbdjlem  47169  squeezedltsq  47603  nthrucw  47607  otiunsndisjX  48016  nltle2tri  48050  icceuelpartlem  48184  lighneallem3  48359  evennodd  48408  oddneven  48409  clnbgrnvtx0  48592  predgclnbgrel  48604  clnbgredg  48605  vopnbgrelself  48620  dfclnbgr6  48621  dfsclnbgr6  48623  clnbgrgrimlem  48698  clnbgrgrim  48699  grlimprclnbgr  48761  usgrexmpl2trifr  48802  gpgusgralem  48821  gpg5nbgrvtx03starlem1  48833  gpg5nbgrvtx03starlem2  48834  gpg5nbgrvtx03starlem3  48835  gpg5nbgrvtx13starlem1  48836  gpg5nbgrvtx13starlem2  48837  gpg5nbgrvtx13starlem3  48838  gpg3nbgrvtx0  48841  gpg3nbgrvtx0ALT  48842  gpg3nbgrvtx1  48843  gpg3kgrtriex  48854  gpg5edgnedg  48895  smprngprmrng  49104  altgsumbcALT  49133  lindslinindsimp1  49237  lindszr  49249  zlmodzxznm  49277  elfzolborelfzop1  49299  blen1b  49368  reorelicc  49490  prelrrx2b  49494  inlinecirc02plem  49566  fvconst0ci  49669