Theorem olcd 888

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm2.48  898  pm2.49  899  orim12i  922  pm1.5  933  animorr  994  animorlr  995  cases2ALT  1064  2nreu  4402  2reu4lem  4479  n0snor2el  4793  disjord  5092  propeqop  5479  somin1  6127  nf1const  7310  soxp  8139  xpord2indlem  8157  naddcllem  8678  fowdom  9558  unxpwdom2  9575  nelaneqOLDOLD  9591  djuunxp  9995  fin1a2lem11  10481  axdc3lem2  10522  gchdomtri  10707  hargch  10751  alephgch  10752  nn1m1nn  12349  nn01to3  13061  rpneg  13147  ltpnf  13242  mnflt  13245  xrlttri  13261  xmulpnf1  13397  iccsplit  13609  elfznelfzo  13901  fvf1tp  13922  addmodlteq  14082  bc0k  14448  bcpasc  14458  hashv01gt1  14482  hashrabsn01  14510  hashsn01  14554  pr2pwpr  14617  hashtpg  14623  ccatsymb  14721  s3sndisj  15113  s3iunsndisj  15114  fsum  15879  fsumsplit  15900  fprod  16101  binomfallfaclem2  16199  fsumdvds  16471  pwp1fsum  16554  lcmfunsnlem1  16805  lcmfunsnlem2  16808  2mulprm  16861  ncoprmlnprm  16897  4sqlem17  17132  vdwlem6  17157  ram0  17193  cshwsidrepswmod0  17265  cshwsdisj  17269  basprssdmsets  17392  mreexfidimd  17817  homffval  17857  comfffval  17865  natfval  18117  xpchomfval  18346  xpccofval  18349  chnccat  18793  plusffval  18815  efmndplusg  19069  smndex1mgm  19099  sgrp2nmndlem5  19121  grpsubfval  19187  grpsubfvalALT  19188  psgnunilem1  19700  psgnunilem5  19701  gsummulg  20149  prmgrpsimpgd  20323  srgbinomlem3  20447  lringuplu  20789  scaffval  21148  drngnidl  21524  cnsubrg  21726  ipffval  21947  lindsdom  22149  psrmulr  22243  pmatcoe1fsupp  23012  en2top  23296  fctop  23315  cctop  23317  metustto  24865  pcofval  25324  pmltpclem2  25763  itg1addlem5  26014  itg10a  26024  dvne0  26324  plyeq0lem  26522  plymullem1  26526  aalioulem4  26655  aalioulem5  26656  aaliou2b  26661  ang180lem3  27132  basellem2  27402  musumsum  27512  dchrhash  27591  lgsdir2lem5  27649  rpvmasumlem  27807  rpvmasum2  27832  pntlemj  27923  ltsres  28012  noetainflem4  28090  addsval  28341  mulsval  28488  mulsproplem13  28507  mulsproplem14  28508  n0s0suc  28721  n0s0m1  28741  nn1m1nns  28753  zseo  28801  halfcut  28837  bdayfinbndlem1  28846  z12zsodd  28861  tgbtwnconn1  29031  tgbtwnconn2  29032  hlid  29068  hltr  29069  hlbtwn  29070  lnhl  29074  colmid  29153  hlpasch  29227  lnincplng  29255  lmieu  29282  lmiinv  29290  cgrahl  29328  cgracol  29329  inaghl  29357  prlngd  29410  edglnl  29714  umgrvad2edg  29787  nbgrnvtx0  29913  wwlksnfi  30488  clwlkclwwlklem2a  30582  clwwlknnn  30617  clwwlknon1nloop  30683  eupth2lem2  30813  frgrwopreg  30917  2wspmdisj  30931  frgrreg  30988  ex-natded5.7  31005  ex-natded5.13  31009  ex-natded9.20  31011  ex-natded9.20-2  31012  aevdemo  31054  f1ocnt  33385  linds2eq  33929  constrextdg2lem  34373  esumsnf  34689  meascnbl  34845  signsplypnf  35172  hashreprin  35242  circlemeth  35262  satfvsucsuc  36109  fmlasucdisj  36143  satfun  36155  satfv1fvfmla1  36167  2goelgoanfmla1  36168  dfrdg4  36695  outsideoftr  36874  lineunray  36892  weiunpo  37233  weiunso  37234  ftc1anclem3  38593  dvasin  38602  areacirclem4  38609  varprop  38622  impprop  38624  smprngopr  38966  tsbi1  39045  tsbi2  39046  lkrshpor  40144  cdleme22b  41378  tendoex  42012  lcfrlem9  42587  aks6d1c2p2  43149  hashnexinjle  43159  grpods  43224  unitscyglem2  43226  pell1234qrdich  43847  acongtr  43964  acongrep  43966  jm2.23  43982  jm2.25  43985  fnwe2lem3  44038  kelac2lem  44050  mendplusgfval  44167  mendmulrfval  44169  onmcl  44317  fzunt  44440  fzuntd  44441  fzunt1d  44442  fzuntgd  44443  ifpim23g  44480  frege122d  44745  clsk1indlem3  45028  refsum2cnlem1  46023  disjxp1  46055  eliuniincex  46093  eliincex  46094  fmul01lt1lem1  46565  limciccioolb  46602  sumnnodd  46611  limcicciooub  46616  wallispilem3  47046  fourierdlem35  47121  fourierdlem80  47165  fourierdlem101  47186  fourierswlem  47209  etransclem32  47245  etransclem35  47248  nnfoctbdjlem  47434  numtowerdt  47885  otiunsndisjX  48318  nltle2tri  48352  icceuelpartlem  48486  lighneallem3  48661  evennodd  48710  oddneven  48711  clnbgrnvtx0  48894  predgclnbgrel  48906  clnbgredg  48907  vopnbgrelself  48922  dfclnbgr6  48923  dfsclnbgr6  48925  clnbgrgrimlem  49000  clnbgrgrim  49001  grlimprclnbgr  49063  usgrexmpl2trifr  49104  gpgusgralem  49123  gpg5nbgrvtx03starlem1  49135  gpg5nbgrvtx03starlem2  49136  gpg5nbgrvtx03starlem3  49137  gpg5nbgrvtx13starlem1  49138  gpg5nbgrvtx13starlem2  49139  gpg5nbgrvtx13starlem3  49140  gpg3nbgrvtx0  49143  gpg3nbgrvtx0ALT  49144  gpg3nbgrvtx1  49145  gpg3kgrtriex  49156  gpg5edgnedg  49197  smprngprmrng  49405  altgsumbcALT  49434  lindslinindsimp1  49538  lindszr  49550  zlmodzxznm  49578  elfzolborelfzop1  49600  blen1b  49669  reorelicc  49791  prelrrx2b  49795  inlinecirc02plem  49867  fvconst0ci  49968