Theorem olcd 888

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm2.48  898  pm2.49  899  orim12i  922  pm1.5  933  animorr  994  animorlr  995  cases2ALT  1064  2nreu  4405  2reu4lem  4482  n0snor2el  4793  disjord  5097  propeqop  5486  somin1  6145  nf1const  7343  soxp  8178  fnwe2lem4  8185  xpord2indlem  8201  naddcllem  8723  fowdom  9602  unxpwdom2  9619  nelaneqOLDOLD  9635  djuunxp  10039  fin1a2lem11  10527  axdc3lem2  10568  gchdomtri  10753  hargch  10797  alephgch  10798  nn1m1nn  12396  nn01to3  13108  rpneg  13194  ltpnf  13289  mnflt  13292  xrlttri  13308  xmulpnf1  13444  iccsplit  13656  elfznelfzo  13948  fvf1tp  13969  addmodlteq  14129  bc0k  14496  bcpasc  14506  hashv01gt1  14530  hashrabsn01  14558  hashsn01  14602  pr2pwpr  14665  hashtpg  14671  ccatsymb  14769  s3sndisj  15163  s3iunsndisj  15164  fsum  15930  fsumsplit  15951  fprod  16152  binomfallfaclem2  16250  fsumdvds  16522  pwp1fsum  16605  lcmfunsnlem1  16856  lcmfunsnlem2  16859  2mulprm  16912  ncoprmlnprm  16948  4sqlem17  17183  vdwlem6  17208  ram0  17244  cshwsidrepswmod0  17316  cshwsdisj  17320  basprssdmsets  17443  mreexfidimd  17874  homffval  17914  comfffval  17922  natfval  18174  xpchomfval  18403  xpccofval  18406  chnccat  18850  plusffval  18872  efmndplusg  19126  smndex1mgm  19156  sgrp2nmndlem5  19178  grpsubfval  19244  grpsubfvalALT  19245  psgnunilem1  19758  psgnunilem5  19759  gsummulg  20207  prmgrpsimpgd  20381  srgbinomlem3  20505  lringuplu  20847  scaffval  21206  drngnidl  21582  cnsubrg  21787  ipffval  22009  lindsdom  22211  psrmulr  22305  pmatcoe1fsupp  23074  en2top  23358  fctop  23377  cctop  23379  metustto  24927  pcofval  25386  pmltpclem2  25825  itg1addlem5  26076  itg10a  26086  dvne0  26386  plyeq0lem  26584  plymullem1  26588  aalioulem4  26719  aalioulem5  26720  aaliou2b  26725  ang180lem3  27196  basellem2  27466  musumsum  27576  dchrhash  27655  lgsdir2lem5  27713  rpvmasumlem  27871  rpvmasum2  27896  pntlemj  27987  ltsres  28076  noetainflem4  28154  addsval  28405  mulsval  28552  mulsproplem13  28571  mulsproplem14  28572  n0s0suc  28785  n0s0m1  28805  nn1m1nns  28817  zseo  28865  halfcut  28901  bdayfinbndlem1  28910  z12zsodd  28925  tgbtwnconn1  29095  tgbtwnconn2  29096  hlid  29132  hltr  29133  hlbtwn  29134  lnhl  29138  colmid  29217  hlpasch  29291  lnincplng  29319  lmieu  29346  lmiinv  29354  cgrahl  29392  cgracol  29393  inaghl  29421  prlngd  29474  edglnl  29778  umgrvad2edg  29851  nbgrnvtx0  29977  wwlksnfi  30552  clwlkclwwlklem2a  30646  clwwlknnn  30681  clwwlknon1nloop  30747  eupth2lem2  30877  frgrwopreg  30981  2wspmdisj  30995  frgrreg  31052  ex-natded5.7  31069  ex-natded5.13  31073  ex-natded9.20  31075  ex-natded9.20-2  31076  aevdemo  31118  inagcgrasubhl  33106  cgrgptxfr  33110  inagcgratrgmain  33111  cgrainag  33117  f1ocnt  33488  linds2eq  34040  constrextdg2lem  34491  esumsnf  34807  meascnbl  34963  signsplypnf  35290  hashreprin  35360  circlemeth  35380  onprcf1of1ord  36096  satfvsucsuc  36338  fmlasucdisj  36372  satfun  36384  satfv1fvfmla1  36396  2goelgoanfmla1  36397  dfrdg4  36930  outsideoftr  37109  lineunray  37127  weiunpo  37468  weiunso  37469  ftc1anclem3  38881  dvasin  38890  areacirclem4  38897  varprop  38910  impprop  38912  smprngopr  39252  tsbi1  39331  tsbi2  39332  lkrshpor  40430  cdleme22b  41664  tendoex  42298  lcfrlem9  42873  aks6d1c2p2  43435  hashnexinjle  43445  grpods  43510  unitscyglem2  43512  pell1234qrdich  44134  acongtr  44251  acongrep  44253  jm2.23  44269  jm2.25  44272  kelac2lem  44332  mendplusgfval  44444  mendmulrfval  44446  onmcl  44594  fzunt  44717  fzuntd  44718  fzunt1d  44719  fzuntgd  44720  ifpim23g  44757  frege122d  45021  clsk1indlem3  45304  refsum2cnlem1  46328  disjxp1  46360  eliuniincex  46397  eliincex  46398  fmul01lt1lem1  46869  limciccioolb  46906  sumnnodd  46915  limcicciooub  46920  wallispilem3  47350  fourierdlem35  47425  fourierdlem80  47469  fourierdlem101  47490  fourierswlem  47513  etransclem32  47549  etransclem35  47552  nnfoctbdjlem  47738  numtowerdt  48189  otiunsndisjX  48622  nltle2tri  48656  icceuelpartlem  48790  lighneallem3  48965  evennodd  49014  oddneven  49015  clnbgrnvtx0  49198  predgclnbgrel  49210  clnbgredg  49211  vopnbgrelself  49226  dfclnbgr6  49227  dfsclnbgr6  49229  clnbgrgrimlem  49304  clnbgrgrim  49305  grlimprclnbgr  49367  usgrexmpl2trifr  49408  gpgusgralem  49427  gpg5nbgrvtx03starlem1  49439  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx13starlem1  49442  gpg5nbgrvtx13starlem2  49443  gpg5nbgrvtx13starlem3  49444  gpg3nbgrvtx0  49447  gpg3nbgrvtx0ALT  49448  gpg3nbgrvtx1  49449  gpg3kgrtriex  49460  gpg5edgnedg  49501  adcnelaz  49722  smprngprmrng  49767  altgsumbcALT  49796  lindslinindsimp1  49900  lindszr  49912  zlmodzxznm  49940  elfzolborelfzop1  49962  blen1b  50031  reorelicc  50153  fvconst0ci  50336  parhomcl2  51076