Theorem olcd 888

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30769. (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  4412  2reu4lem  4487  n0snor2el  4801  disjord  5101  propeqop  5493  somin1  6136  nf1const  7306  soxp  8127  xpord2indlem  8145  naddcllem  8664  fowdom  9535  unxpwdom2  9552  nelaneqOLDOLD  9568  djuunxp  9918  fin1a2lem11  10404  axdc3lem2  10445  gchdomtri  10624  hargch  10668  alephgch  10669  nn1m1nn  12264  nn01to3  12975  rpneg  13060  ltpnf  13155  mnflt  13158  xrlttri  13174  xmulpnf1  13310  iccsplit  13522  elfznelfzo  13813  fvf1tp  13833  addmodlteq  13993  bc0k  14358  bcpasc  14368  hashv01gt1  14392  hashrabsn01  14420  hashsn01  14464  pr2pwpr  14527  hashtpg  14533  ccatsymb  14631  s3sndisj  15015  s3iunsndisj  15016  fsum  15782  fsumsplit  15803  fprod  16006  binomfallfaclem2  16104  fsumdvds  16376  pwp1fsum  16459  lcmfunsnlem1  16705  lcmfunsnlem2  16708  2mulprm  16761  ncoprmlnprm  16797  4sqlem17  17031  vdwlem6  17056  ram0  17092  cshwsidrepswmod0  17164  cshwsdisj  17168  basprssdmsets  17291  mreexfidimd  17716  homffval  17756  comfffval  17764  natfval  18016  xpchomfval  18245  xpccofval  18248  chnccat  18692  plusffval  18714  efmndplusg  18949  smndex1mgm  18979  sgrp2nmndlem5  19001  grpsubfval  19060  grpsubfvalALT  19061  psgnunilem1  19573  psgnunilem5  19574  gsummulg  20022  prmgrpsimpgd  20196  srgbinomlem3  20320  lringuplu  20658  scaffval  21016  drngnidl  21392  cnsubrg  21592  ipffval  21813  psrmulr  22107  pmatcoe1fsupp  22873  en2top  23157  fctop  23176  cctop  23178  metustto  24725  pcofval  25184  pmltpclem2  25623  itg1addlem5  25874  itg10a  25884  dvne0  26185  plyeq0lem  26382  plymullem1  26386  aalioulem4  26513  aalioulem5  26514  aaliou2b  26519  ang180lem3  26991  basellem2  27261  musumsum  27371  dchrhash  27450  lgsdir2lem5  27508  rpvmasumlem  27666  rpvmasum2  27691  pntlemj  27782  ltsres  27841  noetainflem4  27919  addsval  28170  mulsval  28317  mulsproplem13  28336  mulsproplem14  28337  n0s0suc  28550  n0s0m1  28570  nn1m1nns  28582  zseo  28630  halfcut  28666  bdayfinbndlem1  28675  z12zsodd  28690  tgbtwnconn1  28859  tgbtwnconn2  28860  hlid  28896  hltr  28897  hlbtwn  28898  lnhl  28902  colmid  28980  hlpasch  29053  lnincplng  29081  lmieu  29108  lmiinv  29116  cgrahl  29153  cgracol  29154  inaghl  29177  prlngd  29204  edglnl  29508  umgrvad2edg  29578  nbgrnvtx0  29704  wwlksnfi  30270  clwlkclwwlklem2a  30364  clwwlknnn  30399  clwwlknon1nloop  30465  eupth2lem2  30585  frgrwopreg  30689  2wspmdisj  30703  frgrreg  30760  ex-natded5.7  30777  ex-natded5.13  30781  ex-natded9.20  30783  ex-natded9.20-2  30784  aevdemo  30826  f1ocnt  33160  linds2eq  33707  constrextdg2lem  34151  esumsnf  34467  meascnbl  34622  signsplypnf  34950  hashreprin  35020  circlemeth  35040  satfvsucsuc  35869  fmlasucdisj  35903  satfun  35915  satfv1fvfmla1  35927  2goelgoanfmla1  35928  dfrdg4  36455  outsideoftr  36633  lineunray  36651  weiunpo  37008  weiunso  37009  lindsdom  38297  ftc1anclem3  38378  dvasin  38387  areacirclem4  38394  smprngopr  38735  tsbi1  38814  tsbi2  38815  lkrshpor  39913  cdleme22b  41147  tendoex  41781  lcfrlem9  42356  aks6d1c2p2  42918  hashnexinjle  42928  grpods  42993  unitscyglem2  42995  pell1234qrdich  43620  acongtr  43737  acongrep  43739  jm2.23  43755  jm2.25  43758  fnwe2lem3  43811  kelac2lem  43823  mendplusgfval  43940  mendmulrfval  43942  onmcl  44090  fzunt  44213  fzuntd  44214  fzunt1d  44215  fzuntgd  44216  ifpim23g  44253  frege122d  44518  clsk1indlem3  44801  refsum2cnlem1  45789  disjxp1  45821  eliuniincex  45859  eliincex  45860  fmul01lt1lem1  46332  limciccioolb  46369  sumnnodd  46378  limcicciooub  46383  wallispilem3  46813  fourierdlem35  46888  fourierdlem80  46932  fourierdlem101  46953  fourierswlem  46976  etransclem32  47012  etransclem35  47015  nnfoctbdjlem  47201  squeezedltsq  47635  nthrucw  47639  otiunsndisjX  48048  nltle2tri  48082  icceuelpartlem  48216  lighneallem3  48391  evennodd  48440  oddneven  48441  clnbgrnvtx0  48624  predgclnbgrel  48636  clnbgredg  48637  vopnbgrelself  48652  dfclnbgr6  48653  dfsclnbgr6  48655  clnbgrgrimlem  48730  clnbgrgrim  48731  grlimprclnbgr  48793  usgrexmpl2trifr  48834  gpgusgralem  48853  gpg5nbgrvtx03starlem1  48865  gpg5nbgrvtx03starlem2  48866  gpg5nbgrvtx03starlem3  48867  gpg5nbgrvtx13starlem1  48868  gpg5nbgrvtx13starlem2  48869  gpg5nbgrvtx13starlem3  48870  gpg3nbgrvtx0  48873  gpg3nbgrvtx0ALT  48874  gpg3nbgrvtx1  48875  gpg3kgrtriex  48886  gpg5edgnedg  48927  smprngprmrng  49136  altgsumbcALT  49165  lindslinindsimp1  49269  lindszr  49281  zlmodzxznm  49309  elfzolborelfzop1  49331  blen1b  49400  reorelicc  49522  prelrrx2b  49526  inlinecirc02plem  49598  fvconst0ci  49701