Theorem olcd 872

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

Syntax hints:   → wi 4   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  pm2.48  883  pm2.49  884  orim12i  907  pm1.5  918  animorr  977  animorlr  978  cases2ALT  1047  2nreu  4441  2reu4lem  4525  n0snor2el  4834  disjord  5136  propeqop  5507  somin1  6134  nf1const  7304  soxp  8117  xpord2indlem  8135  naddcllem  8677  fowdom  9568  unxpwdom2  9585  nelaneq  9596  djuunxp  9918  fin1a2lem11  10407  axdc3lem2  10448  gchdomtri  10626  hargch  10670  alephgch  10671  nn1m1nn  12235  nn01to3  12927  rpneg  13008  ltpnf  13102  mnflt  13105  xrlttri  13120  xmulpnf1  13255  iccsplit  13464  elfznelfzo  13739  addmodlteq  13913  bc0k  14273  bcpasc  14283  hashv01gt1  14307  hashrabsn01  14335  hashsn01  14378  pr2pwpr  14442  hashtpg  14448  ccatsymb  14534  s3sndisj  14916  s3iunsndisj  14917  fsum  15668  fsumsplit  15689  fprod  15887  binomfallfaclem2  15986  fsumdvds  16253  pwp1fsum  16336  lcmfunsnlem1  16576  lcmfunsnlem2  16579  2mulprm  16632  ncoprmlnprm  16666  4sqlem17  16896  vdwlem6  16921  ram0  16957  cshwsidrepswmod0  17030  cshwsdisj  17034  basprssdmsets  17159  mreexfidimd  17596  homffval  17636  comfffval  17644  natfval  17899  xpchomfval  18133  xpccofval  18136  plusffval  18569  efmndplusg  18763  smndex1mgm  18790  sgrp2nmndlem5  18812  grpsubfval  18870  grpsubfvalALT  18871  psgnunilem1  19363  psgnunilem5  19364  gsummulg  19812  prmgrpsimpgd  19986  srgbinomlem3  20053  lringuplu  20318  scaffval  20495  drngnidl  20860  cnsubrg  21011  ipffval  21207  psrmulr  21509  pmatcoe1fsupp  22210  en2top  22495  fctop  22514  cctop  22516  metustto  24069  pcofval  24533  pmltpclem2  24973  itg1addlem5  25225  itg10a  25235  dvne0  25535  plyeq0lem  25731  plymullem1  25735  aalioulem4  25855  aalioulem5  25856  aaliou2b  25861  ang180lem3  26323  basellem2  26593  musumsum  26703  dchrhash  26781  lgsdir2lem5  26839  rpvmasumlem  26997  rpvmasum2  27022  pntlemj  27113  sltres  27172  noetainflem4  27250  addsval  27455  mulsval  27575  mulsproplem13  27594  mulsproplem14  27595  tgbtwnconn1  27864  tgbtwnconn2  27865  hlid  27898  hltr  27899  hlbtwn  27900  lnhl  27904  colmid  27977  hlpasch  28045  lmieu  28073  lmiinv  28081  cgrahl  28116  cgracol  28117  inaghl  28134  edglnl  28441  umgrvad2edg  28508  nbgrnvtx0  28634  wwlksnfi  29198  clwlkclwwlklem2a  29289  clwwlknnn  29324  clwwlknon1nloop  29390  eupth2lem2  29510  frgrwopreg  29614  2wspmdisj  29628  frgrreg  29685  ex-natded5.7  29702  ex-natded5.13  29706  ex-natded9.20  29708  ex-natded9.20-2  29709  aevdemo  29751  f1ocnt  32051  linds2eq  32542  esumsnf  33131  meascnbl  33286  signsplypnf  33630  hashreprin  33701  circlemeth  33721  satfvsucsuc  34425  fmlasucdisj  34459  satfun  34471  satfv1fvfmla1  34483  2goelgoanfmla1  34484  dfrdg4  34998  outsideoftr  35176  lineunray  35194  lindsdom  36574  ftc1anclem3  36655  dvasin  36664  areacirclem4  36671  smprngopr  37012  tsbi1  37093  tsbi2  37094  lkrshpor  38069  cdleme22b  39304  tendoex  39938  lcfrlem9  40513  aks6d1c2p2  41049  pell1234qrdich  41687  acongtr  41805  acongrep  41807  jm2.23  41823  jm2.25  41826  fnwe2lem3  41882  kelac2lem  41894  mendplusgfval  42015  mendmulrfval  42017  onmcl  42169  fzunt  42294  fzuntd  42295  fzunt1d  42296  fzuntgd  42297  ifpim23g  42334  frege122d  42599  clsk1indlem3  42882  refsum2cnlem1  43809  disjxp1  43844  eliuniincex  43886  eliincex  43887  fmul01lt1lem1  44385  limciccioolb  44422  sumnnodd  44431  limcicciooub  44438  wallispilem3  44868  fourierdlem35  44943  fourierdlem80  44987  fourierdlem101  45008  fourierswlem  45031  etransclem32  45067  etransclem35  45070  nnfoctbdjlem  45256  otiunsndisjX  46072  nltle2tri  46106  icceuelpartlem  46188  lighneallem3  46360  evennodd  46396  oddneven  46397  isomuspgrlem1  46580  altgsumbcALT  47114  lindslinindsimp1  47222  lindszr  47234  zlmodzxznm  47262  elfzolborelfzop1  47284  blen1b  47358  reorelicc  47480  prelrrx2b  47484  inlinecirc02plem  47556  fvconst0ci  47609