Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30332. (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  4407  2reu4lem  4485  n0snor2el  4797  disjord  5096  propeqop  5467  somin1  6106  nf1const  7279  soxp  8108  xpord2indlem  8126  naddcllem  8640  fowdom  9524  unxpwdom2  9541  nelaneq  9552  djuunxp  9874  fin1a2lem11  10363  axdc3lem2  10404  gchdomtri  10582  hargch  10626  alephgch  10627  nn1m1nn  12207  nn01to3  12900  rpneg  12985  ltpnf  13080  mnflt  13083  xrlttri  13099  xmulpnf1  13234  iccsplit  13446  elfznelfzo  13733  fvf1tp  13751  addmodlteq  13911  bc0k  14276  bcpasc  14286  hashv01gt1  14310  hashrabsn01  14338  hashsn01  14381  pr2pwpr  14444  hashtpg  14450  ccatsymb  14547  s3sndisj  14933  s3iunsndisj  14934  fsum  15686  fsumsplit  15707  fprod  15907  binomfallfaclem2  16006  fsumdvds  16278  pwp1fsum  16361  lcmfunsnlem1  16607  lcmfunsnlem2  16610  2mulprm  16663  ncoprmlnprm  16698  4sqlem17  16932  vdwlem6  16957  ram0  16993  cshwsidrepswmod0  17065  cshwsdisj  17069  basprssdmsets  17191  mreexfidimd  17611  homffval  17651  comfffval  17659  natfval  17911  xpchomfval  18140  xpccofval  18143  plusffval  18573  efmndplusg  18807  smndex1mgm  18834  sgrp2nmndlem5  18856  grpsubfval  18915  grpsubfvalALT  18916  psgnunilem1  19423  psgnunilem5  19424  gsummulg  19872  prmgrpsimpgd  20046  srgbinomlem3  20137  lringuplu  20453  scaffval  20786  drngnidl  21153  cnsubrg  21344  ipffval  21557  psrmulr  21851  pmatcoe1fsupp  22588  en2top  22872  fctop  22891  cctop  22893  metustto  24441  pcofval  24910  pmltpclem2  25350  itg1addlem5  25601  itg10a  25611  dvne0  25916  plyeq0lem  26115  plymullem1  26119  aalioulem4  26243  aalioulem5  26244  aaliou2b  26249  ang180lem3  26721  basellem2  26992  musumsum  27102  dchrhash  27182  lgsdir2lem5  27240  rpvmasumlem  27398  rpvmasum2  27423  pntlemj  27514  sltres  27574  noetainflem4  27652  addsval  27869  mulsval  28012  mulsproplem13  28031  mulsproplem14  28032  n0s0suc  28234  n0s0m1  28252  nn1m1nns  28263  zseo  28308  halfcut  28333  tgbtwnconn1  28502  tgbtwnconn2  28503  hlid  28536  hltr  28537  hlbtwn  28538  lnhl  28542  colmid  28615  hlpasch  28683  lmieu  28711  lmiinv  28719  cgrahl  28754  cgracol  28755  inaghl  28772  edglnl  29070  umgrvad2edg  29140  nbgrnvtx0  29266  wwlksnfi  29836  clwlkclwwlklem2a  29927  clwwlknnn  29962  clwwlknon1nloop  30028  eupth2lem2  30148  frgrwopreg  30252  2wspmdisj  30266  frgrreg  30323  ex-natded5.7  30340  ex-natded5.13  30344  ex-natded9.20  30346  ex-natded9.20-2  30347  aevdemo  30389  f1ocnt  32725  linds2eq  33352  constrextdg2lem  33738  esumsnf  34054  meascnbl  34209  signsplypnf  34541  hashreprin  34611  circlemeth  34631  satfvsucsuc  35352  fmlasucdisj  35386  satfun  35398  satfv1fvfmla1  35410  2goelgoanfmla1  35411  dfrdg4  35939  outsideoftr  36117  lineunray  36135  weiunpo  36453  weiunso  36454  lindsdom  37608  ftc1anclem3  37689  dvasin  37698  areacirclem4  37705  smprngopr  38046  tsbi1  38127  tsbi2  38128  lkrshpor  39100  cdleme22b  40335  tendoex  40969  lcfrlem9  41544  aks6d1c2p2  42107  hashnexinjle  42117  grpods  42182  unitscyglem2  42184  pell1234qrdich  42849  acongtr  42967  acongrep  42969  jm2.23  42985  jm2.25  42988  fnwe2lem3  43041  kelac2lem  43053  mendplusgfval  43170  mendmulrfval  43172  onmcl  43320  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  ifpim23g  43484  frege122d  43749  clsk1indlem3  44032  refsum2cnlem1  45031  disjxp1  45063  eliuniincex  45103  eliincex  45104  fmul01lt1lem1  45582  limciccioolb  45619  sumnnodd  45628  limcicciooub  45635  wallispilem3  46065  fourierdlem35  46140  fourierdlem80  46184  fourierdlem101  46205  fourierswlem  46228  etransclem32  46264  etransclem35  46267  nnfoctbdjlem  46453  squeezedltsq  46887  otiunsndisjX  47277  nltle2tri  47311  icceuelpartlem  47433  lighneallem3  47605  evennodd  47641  oddneven  47642  clnbgrnvtx0  47825  predgclnbgrel  47836  clnbgredg  47837  vopnbgrelself  47852  dfclnbgr6  47853  dfsclnbgr6  47855  clnbgrgrimlem  47930  clnbgrgrim  47931  usgrexmpl2trifr  48025  gpgusgralem  48044  gpg5nbgrvtx03starlem1  48056  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem2  48060  gpg5nbgrvtx13starlem3  48061  gpg3nbgrvtx0  48064  gpg3nbgrvtx0ALT  48065  gpg3nbgrvtx1  48066  gpg3kgrtriex  48077  altgsumbcALT  48338  lindslinindsimp1  48443  lindszr  48455  zlmodzxznm  48483  elfzolborelfzop1  48505  blen1b  48574  reorelicc  48696  prelrrx2b  48700  inlinecirc02plem  48772  fvconst0ci  48876