Theorem olcd 888

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 31013. (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  4401  2reu4lem  4478  n0snor2el  4787  disjord  5091  propeqop  5479  somin1  6129  nf1const  7316  soxp  8147  fnwe2lem4  8154  xpord2indlem  8170  naddcllem  8692  fowdom  9572  unxpwdom2  9589  nelaneqOLDOLD  9605  djuunxp  10009  fin1a2lem11  10495  axdc3lem2  10536  gchdomtri  10721  hargch  10765  alephgch  10766  nn1m1nn  12363  nn01to3  13075  rpneg  13161  ltpnf  13256  mnflt  13259  xrlttri  13275  xmulpnf1  13411  iccsplit  13623  elfznelfzo  13915  fvf1tp  13936  addmodlteq  14096  bc0k  14462  bcpasc  14472  hashv01gt1  14496  hashrabsn01  14524  hashsn01  14568  pr2pwpr  14631  hashtpg  14637  ccatsymb  14735  s3sndisj  15129  s3iunsndisj  15130  fsum  15895  fsumsplit  15916  fprod  16117  binomfallfaclem2  16215  fsumdvds  16487  pwp1fsum  16570  lcmfunsnlem1  16821  lcmfunsnlem2  16824  2mulprm  16877  ncoprmlnprm  16913  4sqlem17  17148  vdwlem6  17173  ram0  17209  cshwsidrepswmod0  17281  cshwsdisj  17285  basprssdmsets  17408  mreexfidimd  17833  homffval  17873  comfffval  17881  natfval  18133  xpchomfval  18362  xpccofval  18365  chnccat  18809  plusffval  18831  efmndplusg  19085  smndex1mgm  19115  sgrp2nmndlem5  19137  grpsubfval  19203  grpsubfvalALT  19204  psgnunilem1  19716  psgnunilem5  19717  gsummulg  20165  prmgrpsimpgd  20339  srgbinomlem3  20463  lringuplu  20805  scaffval  21164  drngnidl  21540  cnsubrg  21742  ipffval  21963  lindsdom  22165  psrmulr  22259  pmatcoe1fsupp  23028  en2top  23312  fctop  23331  cctop  23333  metustto  24881  pcofval  25340  pmltpclem2  25779  itg1addlem5  26030  itg10a  26040  dvne0  26340  plyeq0lem  26538  plymullem1  26542  aalioulem4  26671  aalioulem5  26672  aaliou2b  26677  ang180lem3  27148  basellem2  27418  musumsum  27528  dchrhash  27607  lgsdir2lem5  27665  rpvmasumlem  27823  rpvmasum2  27848  pntlemj  27939  ltsres  28028  noetainflem4  28106  addsval  28357  mulsval  28504  mulsproplem13  28523  mulsproplem14  28524  n0s0suc  28737  n0s0m1  28757  nn1m1nns  28769  zseo  28817  halfcut  28853  bdayfinbndlem1  28862  z12zsodd  28877  tgbtwnconn1  29047  tgbtwnconn2  29048  hlid  29084  hltr  29085  hlbtwn  29086  lnhl  29090  colmid  29169  hlpasch  29243  lnincplng  29271  lmieu  29298  lmiinv  29306  cgrahl  29344  cgracol  29345  inaghl  29373  prlngd  29426  edglnl  29730  umgrvad2edg  29803  nbgrnvtx0  29929  wwlksnfi  30504  clwlkclwwlklem2a  30598  clwwlknnn  30633  clwwlknon1nloop  30699  eupth2lem2  30829  frgrwopreg  30933  2wspmdisj  30947  frgrreg  31004  ex-natded5.7  31021  ex-natded5.13  31025  ex-natded9.20  31027  ex-natded9.20-2  31028  aevdemo  31070  inagcgrasubhl  33058  cgrgptxfr  33062  inagcgratrgmain  33063  cgrainag  33069  f1ocnt  33442  linds2eq  33986  constrextdg2lem  34430  esumsnf  34746  meascnbl  34902  signsplypnf  35229  hashreprin  35299  circlemeth  35319  onprcf1of1ord  35978  satfvsucsuc  36220  fmlasucdisj  36254  satfun  36266  satfv1fvfmla1  36278  2goelgoanfmla1  36279  dfrdg4  36811  outsideoftr  36990  lineunray  37008  weiunpo  37349  weiunso  37350  ftc1anclem3  38722  dvasin  38731  areacirclem4  38738  varprop  38751  impprop  38753  smprngopr  39095  tsbi1  39174  tsbi2  39175  lkrshpor  40273  cdleme22b  41507  tendoex  42141  lcfrlem9  42716  aks6d1c2p2  43278  hashnexinjle  43288  grpods  43353  unitscyglem2  43355  pell1234qrdich  43977  acongtr  44094  acongrep  44096  jm2.23  44112  jm2.25  44115  kelac2lem  44175  mendplusgfval  44292  mendmulrfval  44294  onmcl  44442  fzunt  44565  fzuntd  44566  fzunt1d  44567  fzuntgd  44568  ifpim23g  44605  frege122d  44869  clsk1indlem3  45152  refsum2cnlem1  46162  disjxp1  46194  eliuniincex  46232  eliincex  46233  fmul01lt1lem1  46704  limciccioolb  46741  sumnnodd  46750  limcicciooub  46755  wallispilem3  47185  fourierdlem35  47260  fourierdlem80  47304  fourierdlem101  47325  fourierswlem  47348  etransclem32  47384  etransclem35  47387  nnfoctbdjlem  47573  numtowerdt  48024  otiunsndisjX  48457  nltle2tri  48491  icceuelpartlem  48625  lighneallem3  48800  evennodd  48849  oddneven  48850  clnbgrnvtx0  49033  predgclnbgrel  49045  clnbgredg  49046  vopnbgrelself  49061  dfclnbgr6  49062  dfsclnbgr6  49064  clnbgrgrimlem  49139  clnbgrgrim  49140  grlimprclnbgr  49202  usgrexmpl2trifr  49243  gpgusgralem  49262  gpg5nbgrvtx03starlem1  49274  gpg5nbgrvtx03starlem2  49275  gpg5nbgrvtx03starlem3  49276  gpg5nbgrvtx13starlem1  49277  gpg5nbgrvtx13starlem2  49278  gpg5nbgrvtx13starlem3  49279  gpg3nbgrvtx0  49282  gpg3nbgrvtx0ALT  49283  gpg3nbgrvtx1  49284  gpg3kgrtriex  49295  gpg5edgnedg  49336  smprngprmrng  49544  altgsumbcALT  49573  lindslinindsimp1  49677  lindszr  49689  zlmodzxznm  49717  elfzolborelfzop1  49739  blen1b  49808  reorelicc  49930  fvconst0ci  50113  parhomcl2  50853