Theorem olcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30427. (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  4394  2reu4lem  4474  n0snor2el  4787  disjord  5085  propeqop  5453  somin1  6088  nf1const  7248  soxp  8069  xpord2indlem  8087  naddcllem  8602  fowdom  9474  unxpwdom2  9491  nelaneqOLD  9505  djuunxp  9831  fin1a2lem11  10318  axdc3lem2  10359  gchdomtri  10538  hargch  10582  alephgch  10583  nn1m1nn  12164  nn01to3  12852  rpneg  12937  ltpnf  13032  mnflt  13035  xrlttri  13051  xmulpnf1  13187  iccsplit  13399  elfznelfzo  13687  fvf1tp  13707  addmodlteq  13867  bc0k  14232  bcpasc  14242  hashv01gt1  14266  hashrabsn01  14294  hashsn01  14337  pr2pwpr  14400  hashtpg  14406  ccatsymb  14504  s3sndisj  14888  s3iunsndisj  14889  fsum  15641  fsumsplit  15662  fprod  15862  binomfallfaclem2  15961  fsumdvds  16233  pwp1fsum  16316  lcmfunsnlem1  16562  lcmfunsnlem2  16565  2mulprm  16618  ncoprmlnprm  16653  4sqlem17  16887  vdwlem6  16912  ram0  16948  cshwsidrepswmod0  17020  cshwsdisj  17024  basprssdmsets  17146  mreexfidimd  17571  homffval  17611  comfffval  17619  natfval  17871  xpchomfval  18100  xpccofval  18103  chnccat  18547  plusffval  18569  efmndplusg  18803  smndex1mgm  18830  sgrp2nmndlem5  18852  grpsubfval  18911  grpsubfvalALT  18912  psgnunilem1  19420  psgnunilem5  19421  gsummulg  19869  prmgrpsimpgd  20043  srgbinomlem3  20161  lringuplu  20475  scaffval  20829  drngnidl  21196  cnsubrg  21380  ipffval  21601  psrmulr  21896  pmatcoe1fsupp  22643  en2top  22927  fctop  22946  cctop  22948  metustto  24495  pcofval  24964  pmltpclem2  25404  itg1addlem5  25655  itg10a  25665  dvne0  25970  plyeq0lem  26169  plymullem1  26173  aalioulem4  26297  aalioulem5  26298  aaliou2b  26303  ang180lem3  26775  basellem2  27046  musumsum  27156  dchrhash  27236  lgsdir2lem5  27294  rpvmasumlem  27452  rpvmasum2  27477  pntlemj  27568  sltres  27628  noetainflem4  27706  addsval  27932  mulsval  28078  mulsproplem13  28097  mulsproplem14  28098  n0s0suc  28302  n0s0m1  28321  nn1m1nns  28332  zseo  28380  halfcut  28415  zs12zodd  28431  tgbtwnconn1  28596  tgbtwnconn2  28597  hlid  28630  hltr  28631  hlbtwn  28632  lnhl  28636  colmid  28709  hlpasch  28777  lmieu  28805  lmiinv  28813  cgrahl  28848  cgracol  28849  inaghl  28866  edglnl  29165  umgrvad2edg  29235  nbgrnvtx0  29361  wwlksnfi  29928  clwlkclwwlklem2a  30022  clwwlknnn  30057  clwwlknon1nloop  30123  eupth2lem2  30243  frgrwopreg  30347  2wspmdisj  30361  frgrreg  30418  ex-natded5.7  30435  ex-natded5.13  30439  ex-natded9.20  30441  ex-natded9.20-2  30442  aevdemo  30484  f1ocnt  32829  linds2eq  33411  constrextdg2lem  33854  esumsnf  34170  meascnbl  34325  signsplypnf  34656  hashreprin  34726  circlemeth  34746  satfvsucsuc  35508  fmlasucdisj  35542  satfun  35554  satfv1fvfmla1  35566  2goelgoanfmla1  35567  dfrdg4  36094  outsideoftr  36272  lineunray  36290  weiunpo  36608  weiunso  36609  lindsdom  37754  ftc1anclem3  37835  dvasin  37844  areacirclem4  37851  smprngopr  38192  tsbi1  38273  tsbi2  38274  lkrshpor  39306  cdleme22b  40540  tendoex  41174  lcfrlem9  41749  aks6d1c2p2  42312  hashnexinjle  42322  grpods  42387  unitscyglem2  42389  pell1234qrdich  43045  acongtr  43162  acongrep  43164  jm2.23  43180  jm2.25  43183  fnwe2lem3  43236  kelac2lem  43248  mendplusgfval  43365  mendmulrfval  43367  onmcl  43515  fzunt  43638  fzuntd  43639  fzunt1d  43640  fzuntgd  43641  ifpim23g  43678  frege122d  43943  clsk1indlem3  44226  refsum2cnlem1  45224  disjxp1  45256  eliuniincex  45295  eliincex  45296  fmul01lt1lem1  45772  limciccioolb  45809  sumnnodd  45818  limcicciooub  45823  wallispilem3  46253  fourierdlem35  46328  fourierdlem80  46372  fourierdlem101  46393  fourierswlem  46416  etransclem32  46452  etransclem35  46455  nnfoctbdjlem  46641  nthrucw  47072  squeezedltsq  47074  otiunsndisjX  47467  nltle2tri  47501  icceuelpartlem  47623  lighneallem3  47795  evennodd  47831  oddneven  47832  clnbgrnvtx0  48015  predgclnbgrel  48027  clnbgredg  48028  vopnbgrelself  48043  dfclnbgr6  48044  dfsclnbgr6  48046  clnbgrgrimlem  48121  clnbgrgrim  48122  grlimprclnbgr  48184  usgrexmpl2trifr  48225  gpgusgralem  48244  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem2  48260  gpg5nbgrvtx13starlem3  48261  gpg3nbgrvtx0  48264  gpg3nbgrvtx0ALT  48265  gpg3nbgrvtx1  48266  gpg3kgrtriex  48277  gpg5edgnedg  48318  altgsumbcALT  48541  lindslinindsimp1  48645  lindszr  48657  zlmodzxznm  48685  elfzolborelfzop1  48707  blen1b  48776  reorelicc  48898  prelrrx2b  48902  inlinecirc02plem  48974  fvconst0ci  49078