Theorem olcd 885

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  pm2.48  895  pm2.49  896  orim12i  919  pm1.5  930  animorr  992  animorlr  993  cases2ALT  1060  2nreu  4398  2reu4lem  4477  n0snor2el  4791  disjord  5089  propeqop  5476  somin1  6120  nf1const  7288  soxp  8109  xpord2indlem  8127  naddcllem  8646  fowdom  9519  unxpwdom2  9536  nelaneqOLDOLD  9552  djuunxp  9879  fin1a2lem11  10367  axdc3lem2  10408  gchdomtri  10587  hargch  10631  alephgch  10632  nn1m1nn  12231  nn01to3  12942  rpneg  13027  ltpnf  13122  mnflt  13125  xrlttri  13141  xmulpnf1  13277  iccsplit  13489  elfznelfzo  13779  fvf1tp  13799  addmodlteq  13959  bc0k  14324  bcpasc  14334  hashv01gt1  14358  hashrabsn01  14386  hashsn01  14429  pr2pwpr  14492  hashtpg  14498  ccatsymb  14596  s3sndisj  14980  s3iunsndisj  14981  fsum  15747  fsumsplit  15768  fprod  15971  binomfallfaclem2  16070  fsumdvds  16342  pwp1fsum  16425  lcmfunsnlem1  16671  lcmfunsnlem2  16674  2mulprm  16727  ncoprmlnprm  16763  4sqlem17  16997  vdwlem6  17022  ram0  17058  cshwsidrepswmod0  17130  cshwsdisj  17134  basprssdmsets  17257  mreexfidimd  17682  homffval  17722  comfffval  17730  natfval  17982  xpchomfval  18211  xpccofval  18214  chnccat  18658  plusffval  18680  efmndplusg  18914  smndex1mgm  18944  sgrp2nmndlem5  18966  grpsubfval  19025  grpsubfvalALT  19026  psgnunilem1  19533  psgnunilem5  19534  gsummulg  19982  prmgrpsimpgd  20156  srgbinomlem3  20274  lringuplu  20590  scaffval  20944  drngnidl  21310  cnsubrg  21476  ipffval  21697  psrmulr  21991  pmatcoe1fsupp  22758  en2top  23042  fctop  23061  cctop  23063  metustto  24610  pcofval  25069  pmltpclem2  25508  itg1addlem5  25759  itg10a  25769  dvne0  26070  plyeq0lem  26267  plymullem1  26271  aalioulem4  26396  aalioulem5  26397  aaliou2b  26402  ang180lem3  26873  basellem2  27143  musumsum  27253  dchrhash  27332  lgsdir2lem5  27390  rpvmasumlem  27548  rpvmasum2  27573  pntlemj  27664  ltsres  27723  noetainflem4  27801  addsval  28052  mulsval  28199  mulsproplem13  28218  mulsproplem14  28219  n0s0suc  28432  n0s0m1  28452  nn1m1nns  28464  zseo  28512  halfcut  28548  bdayfinbndlem1  28557  z12zsodd  28572  tgbtwnconn1  28741  tgbtwnconn2  28742  hlid  28775  hltr  28776  hlbtwn  28777  lnhl  28781  colmid  28858  hlpasch  28926  lmieu  28954  lmiinv  28962  lnincplng  28988  cgrahl  29018  cgracol  29019  inaghl  29036  prlngd  29063  edglnl  29341  umgrvad2edg  29411  nbgrnvtx0  29537  wwlksnfi  30103  clwlkclwwlklem2a  30197  clwwlknnn  30232  clwwlknon1nloop  30298  eupth2lem2  30418  frgrwopreg  30522  2wspmdisj  30536  frgrreg  30593  ex-natded5.7  30610  ex-natded5.13  30614  ex-natded9.20  30616  ex-natded9.20-2  30617  aevdemo  30659  f1ocnt  32999  linds2eq  33564  constrextdg2lem  34042  esumsnf  34358  meascnbl  34513  signsplypnf  34841  hashreprin  34911  circlemeth  34931  satfvsucsuc  35712  fmlasucdisj  35746  satfun  35758  satfv1fvfmla1  35770  2goelgoanfmla1  35771  dfrdg4  36298  outsideoftr  36476  lineunray  36494  weiunpo  36822  weiunso  36823  lindsdom  38110  ftc1anclem3  38191  dvasin  38200  areacirclem4  38207  smprngopr  38548  tsbi1  38629  tsbi2  38630  lkrshpor  39728  cdleme22b  40962  tendoex  41596  lcfrlem9  42171  aks6d1c2p2  42733  hashnexinjle  42743  grpods  42808  unitscyglem2  42810  pell1234qrdich  43435  acongtr  43552  acongrep  43554  jm2.23  43570  jm2.25  43573  fnwe2lem3  43626  kelac2lem  43638  mendplusgfval  43755  mendmulrfval  43757  onmcl  43905  fzunt  44028  fzuntd  44029  fzunt1d  44030  fzuntgd  44031  ifpim23g  44068  frege122d  44333  clsk1indlem3  44616  refsum2cnlem1  45614  disjxp1  45646  eliuniincex  45684  eliincex  45685  fmul01lt1lem1  46157  limciccioolb  46194  sumnnodd  46203  limcicciooub  46208  wallispilem3  46638  fourierdlem35  46713  fourierdlem80  46757  fourierdlem101  46778  fourierswlem  46801  etransclem32  46837  etransclem35  46840  nnfoctbdjlem  47026  nthrucw  47459  squeezedltsq  47461  otiunsndisjX  47870  nltle2tri  47904  icceuelpartlem  48038  lighneallem3  48213  evennodd  48262  oddneven  48263  clnbgrnvtx0  48446  predgclnbgrel  48458  clnbgredg  48459  vopnbgrelself  48474  dfclnbgr6  48475  dfsclnbgr6  48477  clnbgrgrimlem  48552  clnbgrgrim  48553  grlimprclnbgr  48615  usgrexmpl2trifr  48656  gpgusgralem  48675  gpg5nbgrvtx03starlem1  48687  gpg5nbgrvtx03starlem2  48688  gpg5nbgrvtx03starlem3  48689  gpg5nbgrvtx13starlem1  48690  gpg5nbgrvtx13starlem2  48691  gpg5nbgrvtx13starlem3  48692  gpg3nbgrvtx0  48695  gpg3nbgrvtx0ALT  48696  gpg3nbgrvtx1  48697  gpg3kgrtriex  48708  gpg5edgnedg  48749  altgsumbcALT  48972  lindslinindsimp1  49076  lindszr  49088  zlmodzxznm  49116  elfzolborelfzop1  49138  blen1b  49207  reorelicc  49329  prelrrx2b  49333  inlinecirc02plem  49405  fvconst0ci  49509