Theorem olcd 887

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30694. (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  1062  2nreu  4415  2reu4lem  4489  n0snor2el  4802  disjord  5102  propeqop  5491  somin1  6134  nf1const  7303  soxp  8124  xpord2indlem  8142  naddcllem  8661  fowdom  9532  unxpwdom2  9549  nelaneqOLDOLD  9565  djuunxp  9906  fin1a2lem11  10393  axdc3lem2  10434  gchdomtri  10613  hargch  10657  alephgch  10658  nn1m1nn  12253  nn01to3  12964  rpneg  13049  ltpnf  13144  mnflt  13147  xrlttri  13163  xmulpnf1  13299  iccsplit  13511  elfznelfzo  13801  fvf1tp  13821  addmodlteq  13981  bc0k  14346  bcpasc  14356  hashv01gt1  14380  hashrabsn01  14408  hashsn01  14452  pr2pwpr  14515  hashtpg  14521  ccatsymb  14619  s3sndisj  15003  s3iunsndisj  15004  fsum  15770  fsumsplit  15791  fprod  15994  binomfallfaclem2  16093  fsumdvds  16365  pwp1fsum  16448  lcmfunsnlem1  16694  lcmfunsnlem2  16697  2mulprm  16750  ncoprmlnprm  16786  4sqlem17  17020  vdwlem6  17045  ram0  17081  cshwsidrepswmod0  17153  cshwsdisj  17157  basprssdmsets  17280  mreexfidimd  17705  homffval  17745  comfffval  17753  natfval  18005  xpchomfval  18234  xpccofval  18237  chnccat  18681  plusffval  18703  efmndplusg  18938  smndex1mgm  18968  sgrp2nmndlem5  18990  grpsubfval  19049  grpsubfvalALT  19050  psgnunilem1  19562  psgnunilem5  19563  gsummulg  20011  prmgrpsimpgd  20185  srgbinomlem3  20309  lringuplu  20628  scaffval  20978  drngnidl  21350  cnsubrg  21545  ipffval  21766  psrmulr  22060  pmatcoe1fsupp  22826  en2top  23110  fctop  23129  cctop  23131  metustto  24678  pcofval  25137  pmltpclem2  25576  itg1addlem5  25827  itg10a  25837  dvne0  26138  plyeq0lem  26335  plymullem1  26339  aalioulem4  26464  aalioulem5  26465  aaliou2b  26470  ang180lem3  26941  basellem2  27211  musumsum  27321  dchrhash  27400  lgsdir2lem5  27458  rpvmasumlem  27616  rpvmasum2  27641  pntlemj  27732  ltsres  27791  noetainflem4  27869  addsval  28120  mulsval  28267  mulsproplem13  28286  mulsproplem14  28287  n0s0suc  28500  n0s0m1  28520  nn1m1nns  28532  zseo  28580  halfcut  28616  bdayfinbndlem1  28625  z12zsodd  28640  tgbtwnconn1  28809  tgbtwnconn2  28810  hlid  28843  hltr  28844  hlbtwn  28845  lnhl  28849  colmid  28926  hlpasch  28996  lnincplng  29023  lmieu  29050  lmiinv  29058  cgrahl  29094  cgracol  29095  inaghl  29116  prlngd  29143  edglnl  29433  umgrvad2edg  29503  nbgrnvtx0  29629  wwlksnfi  30195  clwlkclwwlklem2a  30289  clwwlknnn  30324  clwwlknon1nloop  30390  eupth2lem2  30510  frgrwopreg  30614  2wspmdisj  30628  frgrreg  30685  ex-natded5.7  30702  ex-natded5.13  30706  ex-natded9.20  30708  ex-natded9.20-2  30709  aevdemo  30751  f1ocnt  33085  linds2eq  33637  constrextdg2lem  34082  esumsnf  34398  meascnbl  34553  signsplypnf  34881  hashreprin  34951  circlemeth  34971  satfvsucsuc  35755  fmlasucdisj  35789  satfun  35801  satfv1fvfmla1  35813  2goelgoanfmla1  35814  dfrdg4  36341  outsideoftr  36519  lineunray  36537  weiunpo  36864  weiunso  36865  lindsdom  38152  ftc1anclem3  38233  dvasin  38242  areacirclem4  38249  smprngopr  38590  tsbi1  38671  tsbi2  38672  lkrshpor  39770  cdleme22b  41004  tendoex  41638  lcfrlem9  42213  aks6d1c2p2  42775  hashnexinjle  42785  grpods  42850  unitscyglem2  42852  pell1234qrdich  43479  acongtr  43596  acongrep  43598  jm2.23  43614  jm2.25  43617  fnwe2lem3  43670  kelac2lem  43682  mendplusgfval  43799  mendmulrfval  43801  onmcl  43949  fzunt  44072  fzuntd  44073  fzunt1d  44074  fzuntgd  44075  ifpim23g  44112  frege122d  44377  clsk1indlem3  44660  refsum2cnlem1  45648  disjxp1  45680  eliuniincex  45718  eliincex  45719  fmul01lt1lem1  46191  limciccioolb  46228  sumnnodd  46237  limcicciooub  46242  wallispilem3  46672  fourierdlem35  46747  fourierdlem80  46791  fourierdlem101  46812  fourierswlem  46835  etransclem32  46871  etransclem35  46874  nnfoctbdjlem  47060  nthrucw  47493  squeezedltsq  47495  otiunsndisjX  47904  nltle2tri  47938  icceuelpartlem  48072  lighneallem3  48247  evennodd  48296  oddneven  48297  clnbgrnvtx0  48480  predgclnbgrel  48492  clnbgredg  48493  vopnbgrelself  48508  dfclnbgr6  48509  dfsclnbgr6  48511  clnbgrgrimlem  48586  clnbgrgrim  48587  grlimprclnbgr  48649  usgrexmpl2trifr  48690  gpgusgralem  48709  gpg5nbgrvtx03starlem1  48721  gpg5nbgrvtx03starlem2  48722  gpg5nbgrvtx03starlem3  48723  gpg5nbgrvtx13starlem1  48724  gpg5nbgrvtx13starlem2  48725  gpg5nbgrvtx13starlem3  48726  gpg3nbgrvtx0  48729  gpg3nbgrvtx0ALT  48730  gpg3nbgrvtx1  48731  gpg3kgrtriex  48742  gpg5edgnedg  48783  smprngprmrng  48992  altgsumbcALT  49017  lindslinindsimp1  49121  lindszr  49133  zlmodzxznm  49161  elfzolborelfzop1  49183  blen1b  49252  reorelicc  49374  prelrrx2b  49378  inlinecirc02plem  49450  fvconst0ci  49553