Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30369. (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  4426  2reu4lem  4504  n0snor2el  4815  disjord  5114  propeqop  5494  somin1  6135  nf1const  7307  soxp  8137  xpord2indlem  8155  naddcllem  8697  fowdom  9594  unxpwdom2  9611  nelaneq  9622  djuunxp  9944  fin1a2lem11  10433  axdc3lem2  10474  gchdomtri  10652  hargch  10696  alephgch  10697  nn1m1nn  12270  nn01to3  12966  rpneg  13050  ltpnf  13145  mnflt  13148  xrlttri  13164  xmulpnf1  13299  iccsplit  13508  elfznelfzo  13794  fvf1tp  13812  addmodlteq  13970  bc0k  14333  bcpasc  14343  hashv01gt1  14367  hashrabsn01  14395  hashsn01  14438  pr2pwpr  14501  hashtpg  14507  ccatsymb  14603  s3sndisj  14989  s3iunsndisj  14990  fsum  15739  fsumsplit  15760  fprod  15960  binomfallfaclem2  16059  fsumdvds  16328  pwp1fsum  16411  lcmfunsnlem1  16657  lcmfunsnlem2  16660  2mulprm  16713  ncoprmlnprm  16748  4sqlem17  16982  vdwlem6  17007  ram0  17043  cshwsidrepswmod0  17115  cshwsdisj  17119  basprssdmsets  17242  mreexfidimd  17669  homffval  17709  comfffval  17717  natfval  17970  xpchomfval  18199  xpccofval  18202  plusffval  18633  efmndplusg  18867  smndex1mgm  18894  sgrp2nmndlem5  18916  grpsubfval  18975  grpsubfvalALT  18976  psgnunilem1  19484  psgnunilem5  19485  gsummulg  19933  prmgrpsimpgd  20107  srgbinomlem3  20198  lringuplu  20517  scaffval  20851  drngnidl  21220  cnsubrg  21412  ipffval  21633  psrmulr  21929  pmatcoe1fsupp  22674  en2top  22958  fctop  22977  cctop  22979  metustto  24529  pcofval  24998  pmltpclem2  25439  itg1addlem5  25690  itg10a  25700  dvne0  26005  plyeq0lem  26204  plymullem1  26208  aalioulem4  26332  aalioulem5  26333  aaliou2b  26338  ang180lem3  26809  basellem2  27080  musumsum  27190  dchrhash  27270  lgsdir2lem5  27328  rpvmasumlem  27486  rpvmasum2  27511  pntlemj  27602  sltres  27662  noetainflem4  27740  addsval  27950  mulsval  28090  mulsproplem13  28109  mulsproplem14  28110  n0s0suc  28300  n0s0m1  28314  zseo  28361  halfcut  28371  tgbtwnconn1  28538  tgbtwnconn2  28539  hlid  28572  hltr  28573  hlbtwn  28574  lnhl  28578  colmid  28651  hlpasch  28719  lmieu  28747  lmiinv  28755  cgrahl  28790  cgracol  28791  inaghl  28808  edglnl  29107  umgrvad2edg  29177  nbgrnvtx0  29303  wwlksnfi  29873  clwlkclwwlklem2a  29964  clwwlknnn  29999  clwwlknon1nloop  30065  eupth2lem2  30185  frgrwopreg  30289  2wspmdisj  30303  frgrreg  30360  ex-natded5.7  30377  ex-natded5.13  30381  ex-natded9.20  30383  ex-natded9.20-2  30384  aevdemo  30426  f1ocnt  32751  linds2eq  33350  constrextdg2lem  33730  esumsnf  34006  meascnbl  34161  signsplypnf  34506  hashreprin  34576  circlemeth  34596  satfvsucsuc  35311  fmlasucdisj  35345  satfun  35357  satfv1fvfmla1  35369  2goelgoanfmla1  35370  dfrdg4  35893  outsideoftr  36071  lineunray  36089  weiunpo  36407  weiunso  36408  lindsdom  37562  ftc1anclem3  37643  dvasin  37652  areacirclem4  37659  smprngopr  38000  tsbi1  38081  tsbi2  38082  lkrshpor  39049  cdleme22b  40284  tendoex  40918  lcfrlem9  41493  aks6d1c2p2  42061  hashnexinjle  42071  grpods  42136  unitscyglem2  42138  pell1234qrdich  42817  acongtr  42935  acongrep  42937  jm2.23  42953  jm2.25  42956  fnwe2lem3  43009  kelac2lem  43021  mendplusgfval  43138  mendmulrfval  43140  onmcl  43289  fzunt  43413  fzuntd  43414  fzunt1d  43415  fzuntgd  43416  ifpim23g  43453  frege122d  43718  clsk1indlem3  44001  refsum2cnlem1  44987  disjxp1  45019  eliuniincex  45059  eliincex  45060  fmul01lt1lem1  45544  limciccioolb  45581  sumnnodd  45590  limcicciooub  45597  wallispilem3  46027  fourierdlem35  46102  fourierdlem80  46146  fourierdlem101  46167  fourierswlem  46190  etransclem32  46226  etransclem35  46229  nnfoctbdjlem  46415  squeezedltsq  46849  otiunsndisjX  47237  nltle2tri  47271  icceuelpartlem  47368  lighneallem3  47540  evennodd  47576  oddneven  47577  clnbgrnvtx0  47760  predgclnbgrel  47771  clnbgredg  47772  vopnbgrelself  47787  dfclnbgr6  47788  dfsclnbgr6  47790  clnbgrgrimlem  47847  clnbgrgrim  47848  usgrexmpl2trifr  47942  gpgusgralem  47957  gpg5nbgrvtx03starlem1  47970  gpg5nbgrvtx03starlem2  47971  gpg5nbgrvtx03starlem3  47972  gpg5nbgrvtx13starlem1  47973  gpg5nbgrvtx13starlem2  47974  gpg5nbgrvtx13starlem3  47975  gpg3nbgrvtx0  47978  gpg3nbgrvtx0ALT  47979  gpg3nbgrvtx1  47980  gpg3kgrtriex  47991  altgsumbcALT  48215  lindslinindsimp1  48320  lindszr  48332  zlmodzxznm  48360  elfzolborelfzop1  48382  blen1b  48455  reorelicc  48577  prelrrx2b  48581  inlinecirc02plem  48653  fvconst0ci  48737