Theorem olcd 875

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

Syntax hints:   → wi 4   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  pm2.48  885  pm2.49  886  orim12i  909  pm1.5  920  animorr  981  animorlr  982  cases2ALT  1049  2nreu  4398  2reu4lem  4478  n0snor2el  4791  disjord  5089  propeqop  5463  somin1  6098  nf1const  7260  soxp  8081  xpord2indlem  8099  naddcllem  8614  fowdom  9488  unxpwdom2  9505  nelaneqOLD  9519  djuunxp  9845  fin1a2lem11  10332  axdc3lem2  10373  gchdomtri  10552  hargch  10596  alephgch  10597  nn1m1nn  12178  nn01to3  12866  rpneg  12951  ltpnf  13046  mnflt  13049  xrlttri  13065  xmulpnf1  13201  iccsplit  13413  elfznelfzo  13701  fvf1tp  13721  addmodlteq  13881  bc0k  14246  bcpasc  14256  hashv01gt1  14280  hashrabsn01  14308  hashsn01  14351  pr2pwpr  14414  hashtpg  14420  ccatsymb  14518  s3sndisj  14902  s3iunsndisj  14903  fsum  15655  fsumsplit  15676  fprod  15876  binomfallfaclem2  15975  fsumdvds  16247  pwp1fsum  16330  lcmfunsnlem1  16576  lcmfunsnlem2  16579  2mulprm  16632  ncoprmlnprm  16667  4sqlem17  16901  vdwlem6  16926  ram0  16962  cshwsidrepswmod0  17034  cshwsdisj  17038  basprssdmsets  17160  mreexfidimd  17585  homffval  17625  comfffval  17633  natfval  17885  xpchomfval  18114  xpccofval  18117  chnccat  18561  plusffval  18583  efmndplusg  18817  smndex1mgm  18844  sgrp2nmndlem5  18866  grpsubfval  18925  grpsubfvalALT  18926  psgnunilem1  19434  psgnunilem5  19435  gsummulg  19883  prmgrpsimpgd  20057  srgbinomlem3  20175  lringuplu  20489  scaffval  20843  drngnidl  21210  cnsubrg  21394  ipffval  21615  psrmulr  21910  pmatcoe1fsupp  22657  en2top  22941  fctop  22960  cctop  22962  metustto  24509  pcofval  24978  pmltpclem2  25418  itg1addlem5  25669  itg10a  25679  dvne0  25984  plyeq0lem  26183  plymullem1  26187  aalioulem4  26311  aalioulem5  26312  aaliou2b  26317  ang180lem3  26789  basellem2  27060  musumsum  27170  dchrhash  27250  lgsdir2lem5  27308  rpvmasumlem  27466  rpvmasum2  27491  pntlemj  27582  ltsres  27642  noetainflem4  27720  addsval  27970  mulsval  28117  mulsproplem13  28136  mulsproplem14  28137  n0s0suc  28350  n0s0m1  28370  nn1m1nns  28382  zseo  28430  halfcut  28466  bdayfinbndlem1  28475  z12zsodd  28490  tgbtwnconn1  28659  tgbtwnconn2  28660  hlid  28693  hltr  28694  hlbtwn  28695  lnhl  28699  colmid  28772  hlpasch  28840  lmieu  28868  lmiinv  28876  cgrahl  28911  cgracol  28912  inaghl  28929  edglnl  29228  umgrvad2edg  29298  nbgrnvtx0  29424  wwlksnfi  29991  clwlkclwwlklem2a  30085  clwwlknnn  30120  clwwlknon1nloop  30186  eupth2lem2  30306  frgrwopreg  30410  2wspmdisj  30424  frgrreg  30481  ex-natded5.7  30498  ex-natded5.13  30502  ex-natded9.20  30504  ex-natded9.20-2  30505  aevdemo  30547  f1ocnt  32891  linds2eq  33474  constrextdg2lem  33926  esumsnf  34242  meascnbl  34397  signsplypnf  34728  hashreprin  34798  circlemeth  34818  satfvsucsuc  35581  fmlasucdisj  35615  satfun  35627  satfv1fvfmla1  35639  2goelgoanfmla1  35640  dfrdg4  36167  outsideoftr  36345  lineunray  36363  weiunpo  36681  weiunso  36682  lindsdom  37865  ftc1anclem3  37946  dvasin  37955  areacirclem4  37962  smprngopr  38303  tsbi1  38384  tsbi2  38385  lkrshpor  39483  cdleme22b  40717  tendoex  41351  lcfrlem9  41926  aks6d1c2p2  42489  hashnexinjle  42499  grpods  42564  unitscyglem2  42566  pell1234qrdich  43218  acongtr  43335  acongrep  43337  jm2.23  43353  jm2.25  43356  fnwe2lem3  43409  kelac2lem  43421  mendplusgfval  43538  mendmulrfval  43540  onmcl  43688  fzunt  43811  fzuntd  43812  fzunt1d  43813  fzuntgd  43814  ifpim23g  43851  frege122d  44116  clsk1indlem3  44399  refsum2cnlem1  45397  disjxp1  45429  eliuniincex  45468  eliincex  45469  fmul01lt1lem1  45944  limciccioolb  45981  sumnnodd  45990  limcicciooub  45995  wallispilem3  46425  fourierdlem35  46500  fourierdlem80  46544  fourierdlem101  46565  fourierswlem  46588  etransclem32  46624  etransclem35  46627  nnfoctbdjlem  46813  nthrucw  47244  squeezedltsq  47246  otiunsndisjX  47639  nltle2tri  47673  icceuelpartlem  47795  lighneallem3  47967  evennodd  48003  oddneven  48004  clnbgrnvtx0  48187  predgclnbgrel  48199  clnbgredg  48200  vopnbgrelself  48215  dfclnbgr6  48216  dfsclnbgr6  48218  clnbgrgrimlem  48293  clnbgrgrim  48294  grlimprclnbgr  48356  usgrexmpl2trifr  48397  gpgusgralem  48416  gpg5nbgrvtx03starlem1  48428  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx03starlem3  48430  gpg5nbgrvtx13starlem1  48431  gpg5nbgrvtx13starlem2  48432  gpg5nbgrvtx13starlem3  48433  gpg3nbgrvtx0  48436  gpg3nbgrvtx0ALT  48437  gpg3nbgrvtx1  48438  gpg3kgrtriex  48449  gpg5edgnedg  48490  altgsumbcALT  48713  lindslinindsimp1  48817  lindszr  48829  zlmodzxznm  48857  elfzolborelfzop1  48879  blen1b  48948  reorelicc  49070  prelrrx2b  49074  inlinecirc02plem  49146  fvconst0ci  49250