Theorem olcd 875

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 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  4385  2reu4lem  4464  n0snor2el  4777  disjord  5075  propeqop  5456  somin1  6091  nf1const  7253  soxp  8073  xpord2indlem  8091  naddcllem  8606  fowdom  9480  unxpwdom2  9497  nelaneqOLDOLD  9512  djuunxp  9839  fin1a2lem11  10326  axdc3lem2  10367  gchdomtri  10546  hargch  10590  alephgch  10591  nn1m1nn  12189  nn01to3  12885  rpneg  12970  ltpnf  13065  mnflt  13068  xrlttri  13084  xmulpnf1  13220  iccsplit  13432  elfznelfzo  13722  fvf1tp  13742  addmodlteq  13902  bc0k  14267  bcpasc  14277  hashv01gt1  14301  hashrabsn01  14329  hashsn01  14372  pr2pwpr  14435  hashtpg  14441  ccatsymb  14539  s3sndisj  14923  s3iunsndisj  14924  fsum  15676  fsumsplit  15697  fprod  15900  binomfallfaclem2  15999  fsumdvds  16271  pwp1fsum  16354  lcmfunsnlem1  16600  lcmfunsnlem2  16603  2mulprm  16656  ncoprmlnprm  16692  4sqlem17  16926  vdwlem6  16951  ram0  16987  cshwsidrepswmod0  17059  cshwsdisj  17063  basprssdmsets  17185  mreexfidimd  17610  homffval  17650  comfffval  17658  natfval  17910  xpchomfval  18139  xpccofval  18142  chnccat  18586  plusffval  18608  efmndplusg  18842  smndex1mgm  18872  sgrp2nmndlem5  18894  grpsubfval  18953  grpsubfvalALT  18954  psgnunilem1  19462  psgnunilem5  19463  gsummulg  19911  prmgrpsimpgd  20085  srgbinomlem3  20203  lringuplu  20515  scaffval  20869  drngnidl  21236  cnsubrg  21420  ipffval  21641  psrmulr  21934  pmatcoe1fsupp  22679  en2top  22963  fctop  22982  cctop  22984  metustto  24531  pcofval  24990  pmltpclem2  25429  itg1addlem5  25680  itg10a  25690  dvne0  25991  plyeq0lem  26188  plymullem1  26192  aalioulem4  26315  aalioulem5  26316  aaliou2b  26321  ang180lem3  26791  basellem2  27062  musumsum  27172  dchrhash  27251  lgsdir2lem5  27309  rpvmasumlem  27467  rpvmasum2  27492  pntlemj  27583  ltsres  27643  noetainflem4  27721  addsval  27971  mulsval  28118  mulsproplem13  28137  mulsproplem14  28138  n0s0suc  28351  n0s0m1  28371  nn1m1nns  28383  zseo  28431  halfcut  28467  bdayfinbndlem1  28476  z12zsodd  28491  tgbtwnconn1  28660  tgbtwnconn2  28661  hlid  28694  hltr  28695  hlbtwn  28696  lnhl  28700  colmid  28773  hlpasch  28841  lmieu  28869  lmiinv  28877  cgrahl  28912  cgracol  28913  inaghl  28930  edglnl  29229  umgrvad2edg  29299  nbgrnvtx0  29425  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  32891  linds2eq  33459  constrextdg2lem  33911  esumsnf  34227  meascnbl  34382  signsplypnf  34713  hashreprin  34783  circlemeth  34803  satfvsucsuc  35566  fmlasucdisj  35600  satfun  35612  satfv1fvfmla1  35624  2goelgoanfmla1  35625  dfrdg4  36152  outsideoftr  36330  lineunray  36348  weiunpo  36666  weiunso  36667  lindsdom  37952  ftc1anclem3  38033  dvasin  38042  areacirclem4  38049  smprngopr  38390  tsbi1  38471  tsbi2  38472  lkrshpor  39570  cdleme22b  40804  tendoex  41438  lcfrlem9  42013  aks6d1c2p2  42575  hashnexinjle  42585  grpods  42650  unitscyglem2  42652  pell1234qrdich  43310  acongtr  43427  acongrep  43429  jm2.23  43445  jm2.25  43448  fnwe2lem3  43501  kelac2lem  43513  mendplusgfval  43630  mendmulrfval  43632  onmcl  43780  fzunt  43903  fzuntd  43904  fzunt1d  43905  fzuntgd  43906  ifpim23g  43943  frege122d  44208  clsk1indlem3  44491  refsum2cnlem1  45489  disjxp1  45521  eliuniincex  45560  eliincex  45561  fmul01lt1lem1  46035  limciccioolb  46072  sumnnodd  46081  limcicciooub  46086  wallispilem3  46516  fourierdlem35  46591  fourierdlem80  46635  fourierdlem101  46656  fourierswlem  46679  etransclem32  46715  etransclem35  46718  nnfoctbdjlem  46904  nthrucw  47335  squeezedltsq  47337  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