Theorem olcd 880

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

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  pm2.48  890  pm2.49  891  orim12i  914  pm1.5  925  animorr  986  animorlr  987  cases2ALT  1054  2nreu  4372  2reu4lem  4451  n0snor2el  4764  disjord  5061  propeqop  5448  somin1  6083  nf1const  7248  soxp  8069  xpord2indlem  8087  naddcllem  8602  fowdom  9476  unxpwdom2  9493  nelaneqOLDOLD  9509  djuunxp  9836  fin1a2lem11  10323  axdc3lem2  10364  gchdomtri  10543  hargch  10587  alephgch  10588  nn1m1nn  12186  nn01to3  12882  rpneg  12967  ltpnf  13062  mnflt  13065  xrlttri  13081  xmulpnf1  13217  iccsplit  13429  elfznelfzo  13719  fvf1tp  13739  addmodlteq  13899  bc0k  14264  bcpasc  14274  hashv01gt1  14298  hashrabsn01  14326  hashsn01  14369  pr2pwpr  14432  hashtpg  14438  ccatsymb  14536  s3sndisj  14920  s3iunsndisj  14921  fsum  15673  fsumsplit  15694  fprod  15897  binomfallfaclem2  15996  fsumdvds  16268  pwp1fsum  16351  lcmfunsnlem1  16597  lcmfunsnlem2  16600  2mulprm  16653  ncoprmlnprm  16689  4sqlem17  16923  vdwlem6  16948  ram0  16984  cshwsidrepswmod0  17056  cshwsdisj  17060  basprssdmsets  17182  mreexfidimd  17607  homffval  17647  comfffval  17655  natfval  17907  xpchomfval  18136  xpccofval  18139  chnccat  18583  plusffval  18605  efmndplusg  18839  smndex1mgm  18869  sgrp2nmndlem5  18891  grpsubfval  18950  grpsubfvalALT  18951  psgnunilem1  19459  psgnunilem5  19460  gsummulg  19908  prmgrpsimpgd  20082  srgbinomlem3  20200  lringuplu  20516  scaffval  20870  drngnidl  21236  cnsubrg  21402  ipffval  21623  psrmulr  21917  pmatcoe1fsupp  22684  en2top  22968  fctop  22987  cctop  22989  metustto  24536  pcofval  24995  pmltpclem2  25434  itg1addlem5  25685  itg10a  25695  dvne0  25996  plyeq0lem  26193  plymullem1  26197  aalioulem4  26319  aalioulem5  26320  aaliou2b  26325  ang180lem3  26793  basellem2  27063  musumsum  27173  dchrhash  27252  lgsdir2lem5  27310  rpvmasumlem  27468  rpvmasum2  27493  pntlemj  27584  ltsres  27644  noetainflem4  27722  addsval  27972  mulsval  28119  mulsproplem13  28138  mulsproplem14  28139  n0s0suc  28352  n0s0m1  28372  nn1m1nns  28384  zseo  28432  halfcut  28468  bdayfinbndlem1  28477  z12zsodd  28492  tgbtwnconn1  28661  tgbtwnconn2  28662  hlid  28695  hltr  28696  hlbtwn  28697  lnhl  28701  colmid  28774  hlpasch  28842  lmieu  28870  lmiinv  28878  cgrahl  28913  cgracol  28914  inaghl  28931  edglnl  29230  umgrvad2edg  29300  nbgrnvtx0  29426  wwlksnfi  29992  clwlkclwwlklem2a  30086  clwwlknnn  30121  clwwlknon1nloop  30187  eupth2lem2  30307  frgrwopreg  30411  2wspmdisj  30425  frgrreg  30482  ex-natded5.7  30499  ex-natded5.13  30503  ex-natded9.20  30505  ex-natded9.20-2  30506  aevdemo  30548  f1ocnt  32892  linds2eq  33464  constrextdg2lem  33932  esumsnf  34248  meascnbl  34403  signsplypnf  34734  hashreprin  34804  circlemeth  34824  satfvsucsuc  35593  fmlasucdisj  35627  satfun  35639  satfv1fvfmla1  35651  2goelgoanfmla1  35652  dfrdg4  36179  outsideoftr  36357  lineunray  36375  weiunpo  36693  weiunso  36694  lindsdom  37981  ftc1anclem3  38062  dvasin  38071  areacirclem4  38078  smprngopr  38419  tsbi1  38500  tsbi2  38501  lkrshpor  39599  cdleme22b  40833  tendoex  41467  lcfrlem9  42042  aks6d1c2p2  42604  hashnexinjle  42614  grpods  42679  unitscyglem2  42681  pell1234qrdich  43306  acongtr  43423  acongrep  43425  jm2.23  43441  jm2.25  43444  fnwe2lem3  43497  kelac2lem  43509  mendplusgfval  43626  mendmulrfval  43628  onmcl  43776  fzunt  43899  fzuntd  43900  fzunt1d  43901  fzuntgd  43902  ifpim23g  43939  frege122d  44204  clsk1indlem3  44487  refsum2cnlem1  45485  disjxp1  45517  eliuniincex  45556  eliincex  45557  fmul01lt1lem1  46029  limciccioolb  46066  sumnnodd  46075  limcicciooub  46080  wallispilem3  46510  fourierdlem35  46585  fourierdlem80  46629  fourierdlem101  46650  fourierswlem  46673  etransclem32  46709  etransclem35  46712  nnfoctbdjlem  46898  nthrucw  47331  squeezedltsq  47333  otiunsndisjX  47742  nltle2tri  47776  icceuelpartlem  47910  lighneallem3  48085  evennodd  48134  oddneven  48135  clnbgrnvtx0  48318  predgclnbgrel  48330  clnbgredg  48331  vopnbgrelself  48346  dfclnbgr6  48347  dfsclnbgr6  48349  clnbgrgrimlem  48424  clnbgrgrim  48425  grlimprclnbgr  48487  usgrexmpl2trifr  48528  gpgusgralem  48547  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg3nbgrvtx0  48567  gpg3nbgrvtx0ALT  48568  gpg3nbgrvtx1  48569  gpg3kgrtriex  48580  gpg5edgnedg  48621  altgsumbcALT  48844  lindslinindsimp1  48948  lindszr  48960  zlmodzxznm  48988  elfzolborelfzop1  49010  blen1b  49079  reorelicc  49201  prelrrx2b  49205  inlinecirc02plem  49277  fvconst0ci  49381