Theorem olcd 874

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

Syntax hints:   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  pm2.48  884  pm2.49  885  orim12i  908  pm1.5  919  animorr  980  animorlr  981  cases2ALT  1048  2nreu  4450  2reu4lem  4528  n0snor2el  4838  disjord  5137  propeqop  5517  somin1  6156  nf1const  7324  soxp  8153  xpord2indlem  8171  naddcllem  8713  fowdom  9609  unxpwdom2  9626  nelaneq  9637  djuunxp  9959  fin1a2lem11  10448  axdc3lem2  10489  gchdomtri  10667  hargch  10711  alephgch  10712  nn1m1nn  12285  nn01to3  12981  rpneg  13065  ltpnf  13160  mnflt  13163  xrlttri  13178  xmulpnf1  13313  iccsplit  13522  elfznelfzo  13808  fvf1tp  13826  addmodlteq  13984  bc0k  14347  bcpasc  14357  hashv01gt1  14381  hashrabsn01  14409  hashsn01  14452  pr2pwpr  14515  hashtpg  14521  ccatsymb  14617  s3sndisj  15003  s3iunsndisj  15004  fsum  15753  fsumsplit  15774  fprod  15974  binomfallfaclem2  16073  fsumdvds  16342  pwp1fsum  16425  lcmfunsnlem1  16671  lcmfunsnlem2  16674  2mulprm  16727  ncoprmlnprm  16762  4sqlem17  16995  vdwlem6  17020  ram0  17056  cshwsidrepswmod0  17129  cshwsdisj  17133  basprssdmsets  17258  mreexfidimd  17695  homffval  17735  comfffval  17743  natfval  18001  xpchomfval  18235  xpccofval  18238  plusffval  18672  efmndplusg  18906  smndex1mgm  18933  sgrp2nmndlem5  18955  grpsubfval  19014  grpsubfvalALT  19015  psgnunilem1  19526  psgnunilem5  19527  gsummulg  19975  prmgrpsimpgd  20149  srgbinomlem3  20246  lringuplu  20561  scaffval  20895  drngnidl  21271  cnsubrg  21463  ipffval  21684  psrmulr  21980  pmatcoe1fsupp  22723  en2top  23008  fctop  23027  cctop  23029  metustto  24582  pcofval  25057  pmltpclem2  25498  itg1addlem5  25750  itg10a  25760  dvne0  26065  plyeq0lem  26264  plymullem1  26268  aalioulem4  26392  aalioulem5  26393  aaliou2b  26398  ang180lem3  26869  basellem2  27140  musumsum  27250  dchrhash  27330  lgsdir2lem5  27388  rpvmasumlem  27546  rpvmasum2  27571  pntlemj  27662  sltres  27722  noetainflem4  27800  addsval  28010  mulsval  28150  mulsproplem13  28169  mulsproplem14  28170  n0s0suc  28360  n0s0m1  28374  zseo  28421  halfcut  28431  tgbtwnconn1  28598  tgbtwnconn2  28599  hlid  28632  hltr  28633  hlbtwn  28634  lnhl  28638  colmid  28711  hlpasch  28779  lmieu  28807  lmiinv  28815  cgrahl  28850  cgracol  28851  inaghl  28868  edglnl  29175  umgrvad2edg  29245  nbgrnvtx0  29371  wwlksnfi  29936  clwlkclwwlklem2a  30027  clwwlknnn  30062  clwwlknon1nloop  30128  eupth2lem2  30248  frgrwopreg  30352  2wspmdisj  30366  frgrreg  30423  ex-natded5.7  30440  ex-natded5.13  30444  ex-natded9.20  30446  ex-natded9.20-2  30447  aevdemo  30489  f1ocnt  32810  linds2eq  33389  esumsnf  34045  meascnbl  34200  signsplypnf  34544  hashreprin  34614  circlemeth  34634  satfvsucsuc  35350  fmlasucdisj  35384  satfun  35396  satfv1fvfmla1  35408  2goelgoanfmla1  35409  dfrdg4  35933  outsideoftr  36111  lineunray  36129  weiunpo  36448  weiunso  36449  lindsdom  37601  ftc1anclem3  37682  dvasin  37691  areacirclem4  37698  smprngopr  38039  tsbi1  38120  tsbi2  38121  lkrshpor  39089  cdleme22b  40324  tendoex  40958  lcfrlem9  41533  aks6d1c2p2  42101  hashnexinjle  42111  grpods  42176  unitscyglem2  42178  pell1234qrdich  42849  acongtr  42967  acongrep  42969  jm2.23  42985  jm2.25  42988  fnwe2lem3  43041  kelac2lem  43053  mendplusgfval  43170  mendmulrfval  43172  onmcl  43321  fzunt  43445  fzuntd  43446  fzunt1d  43447  fzuntgd  43448  ifpim23g  43485  frege122d  43750  clsk1indlem3  44033  refsum2cnlem1  44975  disjxp1  45009  eliuniincex  45049  eliincex  45050  fmul01lt1lem1  45540  limciccioolb  45577  sumnnodd  45586  limcicciooub  45593  wallispilem3  46023  fourierdlem35  46098  fourierdlem80  46142  fourierdlem101  46163  fourierswlem  46186  etransclem32  46222  etransclem35  46225  nnfoctbdjlem  46411  otiunsndisjX  47229  nltle2tri  47263  icceuelpartlem  47360  lighneallem3  47532  evennodd  47568  oddneven  47569  clnbgrnvtx0  47752  predgclnbgrel  47763  clnbgredg  47764  vopnbgrelself  47779  dfclnbgr6  47780  dfsclnbgr6  47782  clnbgrgrimlem  47839  clnbgrgrim  47840  usgrexmpl2trifr  47932  gpgusgralem  47946  gpg5nbgrvtx03starlem1  47959  gpg5nbgrvtx03starlem2  47960  gpg5nbgrvtx03starlem3  47961  gpg5nbgrvtx13starlem1  47962  gpg5nbgrvtx13starlem2  47963  gpg5nbgrvtx13starlem3  47964  gpg3nbgrvtx0  47967  gpg3nbgrvtx0ALT  47968  gpg3nbgrvtx1  47969  altgsumbcALT  48198  lindslinindsimp1  48303  lindszr  48315  zlmodzxznm  48343  elfzolborelfzop1  48365  blen1b  48438  reorelicc  48560  prelrrx2b  48564  inlinecirc02plem  48636  fvconst0ci  48689