Theorem olcd 888

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30825. (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  4409  2reu4lem  4486  n0snor2el  4800  disjord  5100  propeqop  5492  somin1  6135  nf1const  7311  soxp  8131  xpord2indlem  8149  naddcllem  8668  fowdom  9540  unxpwdom2  9557  nelaneqOLDOLD  9573  djuunxp  9923  fin1a2lem11  10409  axdc3lem2  10450  gchdomtri  10629  hargch  10673  alephgch  10674  nn1m1nn  12269  nn01to3  12981  rpneg  13066  ltpnf  13161  mnflt  13164  xrlttri  13180  xmulpnf1  13316  iccsplit  13528  elfznelfzo  13819  fvf1tp  13840  addmodlteq  14000  bc0k  14365  bcpasc  14375  hashv01gt1  14399  hashrabsn01  14427  hashsn01  14471  pr2pwpr  14534  hashtpg  14540  ccatsymb  14638  s3sndisj  15028  s3iunsndisj  15029  fsum  15794  fsumsplit  15815  fprod  16018  binomfallfaclem2  16116  fsumdvds  16388  pwp1fsum  16471  lcmfunsnlem1  16717  lcmfunsnlem2  16720  2mulprm  16773  ncoprmlnprm  16809  4sqlem17  17043  vdwlem6  17068  ram0  17104  cshwsidrepswmod0  17176  cshwsdisj  17180  basprssdmsets  17303  mreexfidimd  17728  homffval  17768  comfffval  17776  natfval  18028  xpchomfval  18257  xpccofval  18260  chnccat  18704  plusffval  18726  efmndplusg  18976  smndex1mgm  19006  sgrp2nmndlem5  19028  grpsubfval  19094  grpsubfvalALT  19095  psgnunilem1  19607  psgnunilem5  19608  gsummulg  20056  prmgrpsimpgd  20230  srgbinomlem3  20354  lringuplu  20693  scaffval  21051  drngnidl  21427  cnsubrg  21627  ipffval  21848  psrmulr  22142  pmatcoe1fsupp  22908  en2top  23192  fctop  23211  cctop  23213  metustto  24761  pcofval  25220  pmltpclem2  25659  itg1addlem5  25910  itg10a  25920  dvne0  26221  plyeq0lem  26418  plymullem1  26422  aalioulem4  26549  aalioulem5  26550  aaliou2b  26555  ang180lem3  27027  basellem2  27297  musumsum  27407  dchrhash  27486  lgsdir2lem5  27544  rpvmasumlem  27702  rpvmasum2  27727  pntlemj  27818  ltsres  27877  noetainflem4  27955  addsval  28206  mulsval  28353  mulsproplem13  28372  mulsproplem14  28373  n0s0suc  28586  n0s0m1  28606  nn1m1nns  28618  zseo  28666  halfcut  28702  bdayfinbndlem1  28711  z12zsodd  28726  tgbtwnconn1  28895  tgbtwnconn2  28896  hlid  28932  hltr  28933  hlbtwn  28934  lnhl  28938  colmid  29016  hlpasch  29089  lnincplng  29117  lmieu  29144  lmiinv  29152  cgrahl  29189  cgracol  29190  inaghl  29217  prlngd  29244  edglnl  29548  umgrvad2edg  29621  nbgrnvtx0  29747  wwlksnfi  30322  clwlkclwwlklem2a  30416  clwwlknnn  30451  clwwlknon1nloop  30517  eupth2lem2  30641  frgrwopreg  30745  2wspmdisj  30759  frgrreg  30816  ex-natded5.7  30833  ex-natded5.13  30837  ex-natded9.20  30839  ex-natded9.20-2  30840  aevdemo  30882  f1ocnt  33215  linds2eq  33758  constrextdg2lem  34202  esumsnf  34518  meascnbl  34674  signsplypnf  35002  hashreprin  35072  circlemeth  35092  satfvsucsuc  35894  fmlasucdisj  35928  satfun  35940  satfv1fvfmla1  35952  2goelgoanfmla1  35953  dfrdg4  36480  outsideoftr  36658  lineunray  36676  weiunpo  37033  weiunso  37034  lindsdom  38322  ftc1anclem3  38403  dvasin  38412  areacirclem4  38419  smprngopr  38761  tsbi1  38840  tsbi2  38841  lkrshpor  39939  cdleme22b  41173  tendoex  41807  lcfrlem9  42382  aks6d1c2p2  42944  hashnexinjle  42954  grpods  43019  unitscyglem2  43021  pell1234qrdich  43646  acongtr  43763  acongrep  43765  jm2.23  43781  jm2.25  43784  fnwe2lem3  43837  kelac2lem  43849  mendplusgfval  43966  mendmulrfval  43968  onmcl  44116  fzunt  44239  fzuntd  44240  fzunt1d  44241  fzuntgd  44242  ifpim23g  44279  frege122d  44544  clsk1indlem3  44827  refsum2cnlem1  45815  disjxp1  45847  eliuniincex  45885  eliincex  45886  fmul01lt1lem1  46358  limciccioolb  46395  sumnnodd  46404  limcicciooub  46409  wallispilem3  46839  fourierdlem35  46914  fourierdlem80  46958  fourierdlem101  46979  fourierswlem  47002  etransclem32  47038  etransclem35  47041  nnfoctbdjlem  47227  squeezedltsq  47661  nthrucw  47665  otiunsndisjX  48074  nltle2tri  48108  icceuelpartlem  48242  lighneallem3  48417  evennodd  48466  oddneven  48467  clnbgrnvtx0  48650  predgclnbgrel  48662  clnbgredg  48663  vopnbgrelself  48678  dfclnbgr6  48679  dfsclnbgr6  48681  clnbgrgrimlem  48756  clnbgrgrim  48757  grlimprclnbgr  48819  usgrexmpl2trifr  48860  gpgusgralem  48879  gpg5nbgrvtx03starlem1  48891  gpg5nbgrvtx03starlem2  48892  gpg5nbgrvtx03starlem3  48893  gpg5nbgrvtx13starlem1  48894  gpg5nbgrvtx13starlem2  48895  gpg5nbgrvtx13starlem3  48896  gpg3nbgrvtx0  48899  gpg3nbgrvtx0ALT  48900  gpg3nbgrvtx1  48901  gpg3kgrtriex  48912  gpg5edgnedg  48953  smprngprmrng  49161  altgsumbcALT  49190  lindslinindsimp1  49294  lindszr  49306  zlmodzxznm  49334  elfzolborelfzop1  49356  blen1b  49425  reorelicc  49547  prelrrx2b  49551  inlinecirc02plem  49623  fvconst0ci  49726