Theorem olcd 870

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

Syntax hints:   → wi 4   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  pm2.48  881  pm2.49  882  orim12i  905  pm1.5  916  animorr  975  animorlr  976  cases2ALT  1043  2nreu  4393  2reu4lem  4465  n0snor2el  4764  disjord  5054  propeqop  5397  somin1  5993  nf1const  7059  soxp  7823  fowdom  9035  unxpwdom2  9052  nelaneq  9063  djuunxp  9350  fin1a2lem11  9832  axdc3lem2  9873  gchdomtri  10051  hargch  10095  alephgch  10096  nn1m1nn  11659  nn01to3  12342  rpneg  12422  ltpnf  12516  mnflt  12519  xrlttri  12533  xmulpnf1  12668  iccsplit  12872  elfznelfzo  13143  addmodlteq  13315  bc0k  13672  bcpasc  13682  hashv01gt1  13706  hashrabsn01  13735  hashsn01  13778  pr2pwpr  13838  hashtpg  13844  ffz0iswrdOLD  13892  ccatsymb  13936  s3sndisj  14327  s3iunsndisj  14328  fsum  15077  fsumsplit  15097  fprod  15295  binomfallfaclem2  15394  fsumdvds  15658  pwp1fsum  15742  lcmfunsnlem1  15981  lcmfunsnlem2  15984  2mulprm  16037  ncoprmlnprm  16068  4sqlem17  16297  vdwlem6  16322  ram0  16358  cshwsidrepswmod0  16428  cshwsdisj  16432  basprssdmsets  16549  mreexfidimd  16921  homffval  16960  comfffval  16968  natfval  17216  xpchomfval  17429  xpccofval  17432  plusffval  17858  efmndplusg  18045  smndex1mgm  18072  sgrp2nmndlem5  18094  grpsubfval  18147  grpsubfvalALT  18148  psgnunilem1  18621  psgnunilem5  18622  gsummulg  19062  prmgrpsimpgd  19236  srgbinomlem3  19292  scaffval  19652  drngnidl  20002  psrmulr  20164  cnsubrg  20605  ipffval  20792  pmatcoe1fsupp  21309  en2top  21593  fctop  21612  cctop  21614  metustto  23163  pcofval  23614  pmltpclem2  24050  itg1addlem5  24301  itg10a  24311  dvne0  24608  plyeq0lem  24800  plymullem1  24804  aalioulem4  24924  aalioulem5  24925  aaliou2b  24930  ang180lem3  25389  basellem2  25659  musumsum  25769  dchrhash  25847  lgsdir2lem5  25905  rpvmasumlem  26063  rpvmasum2  26088  pntlemj  26179  tgbtwnconn1  26361  tgbtwnconn2  26362  hlid  26395  hltr  26396  hlbtwn  26397  lnhl  26401  colmid  26474  hlpasch  26542  lmieu  26570  lmiinv  26578  cgrahl  26613  cgracol  26614  inaghl  26631  edglnl  26928  umgrvad2edg  26995  nbgrnvtx0  27121  wwlksnfi  27684  clwlkclwwlklem2a  27776  clwwlknnn  27811  clwwlknfiOLD  27824  clwwlknon1nloop  27878  eupth2lem2  27998  frgrwopreg  28102  2wspmdisj  28116  frgrreg  28173  ex-natded5.7  28190  ex-natded5.13  28194  ex-natded9.20  28196  ex-natded9.20-2  28197  aevdemo  28239  f1ocnt  30525  linds2eq  30941  esumsnf  31323  meascnbl  31478  signsplypnf  31820  hashreprin  31891  circlemeth  31911  satfvsucsuc  32612  fmlasucdisj  32646  satfun  32658  satfv1fvfmla1  32670  2goelgoanfmla1  32671  sltres  33169  dfrdg4  33412  outsideoftr  33590  lineunray  33608  lindsdom  34901  ftc1anclem3  34984  dvasin  34993  areacirclem4  35000  smprngopr  35345  tsbi1  35426  tsbi2  35427  lkrshpor  36258  cdleme22b  37492  tendoex  38126  lcfrlem9  38701  pell1234qrdich  39478  acongtr  39595  acongrep  39597  jm2.23  39613  jm2.25  39616  fnwe2lem3  39672  kelac2lem  39684  mendplusgfval  39805  mendmulrfval  39807  ifpim23g  39881  frege122d  40125  clsk1indlem3  40413  refsum2cnlem1  41314  disjxp1  41351  eliuniincex  41395  eliincex  41396  fmul01lt1lem1  41885  limciccioolb  41922  sumnnodd  41931  limcicciooub  41938  wallispilem3  42372  fourierdlem35  42447  fourierdlem80  42491  fourierdlem101  42512  fourierswlem  42535  etransclem32  42571  etransclem35  42574  nnfoctbdjlem  42757  otiunsndisjX  43498  nltle2tri  43533  icceuelpartlem  43615  lighneallem3  43792  evennodd  43828  oddneven  43829  isomuspgrlem1  44012  altgsumbcALT  44421  lindslinindsimp1  44532  lindszr  44544  zlmodzxznm  44572  elfzolborelfzop1  44594  blen1b  44668  reorelicc  44717  prelrrx2b  44721  inlinecirc02plem  44793