Theorem olcd 905

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

Syntax hints:   → wi 4   ∨ wo 878

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 199  df-or 879

This theorem is referenced by:  pm2.48  913  pm2.49  914  orim12i  937  pm1.5  948  animorr  1006  animorlr  1007  cases2ALT  1075  n0snor2el  4582  disjord  4864  propeqop  5195  somin1  5775  soxp  7559  fowdom  8752  unxpwdom2  8769  nelaneq  8780  djuunxp  9067  fin1a2lem11  9554  axdc3lem2  9595  gchdomtri  9773  hargch  9817  alephgch  9818  nn1m1nn  11379  nn01to3  12071  rpneg  12153  ltpnf  12247  mnflt  12250  xrlttri  12265  xmulpnf1  12399  iccsplit  12605  elfznelfzo  12875  addmodlteq  13047  bc0k  13398  bcpasc  13408  hashv01gt1  13432  hashrabsn01  13459  hashsn01  13500  hashf1  13537  pr2pwpr  13557  hashtpg  13563  ffz0iswrd  13608  ccatsymb  13649  s3sndisj  14092  s3iunsndisj  14093  fsum  14835  fsumsplit  14855  fprod  15051  binomfallfaclem2  15150  fsumdvds  15414  pwp1fsum  15495  lcmfunsnlem1  15730  lcmfunsnlem2  15733  ncoprmlnprm  15814  sumhash  15978  4sqlem17  16043  vdwlem6  16068  ram0  16104  cshwsidrepswmod0  16174  cshwsdisj  16178  basprssdmsets  16295  mreexfidimd  16670  sgrp2nmndlem5  17777  psgnunilem1  18270  psgnunilem5  18271  psgnunilem5OLD  18272  gsummulg  18702  srgbinomlem3  18903  drngnidl  19597  cnsubrg  20173  pmatcoe1fsupp  20883  mp2pm2mplem4  20991  en2top  21167  fctop  21186  cctop  21188  metustto  22735  pmltpclem2  23622  itg1addlem5  23873  itg10a  23883  dvne0  24180  plyeq0lem  24372  plymullem1  24376  aalioulem4  24496  aalioulem5  24497  aaliou2b  24502  relogbf  24938  logblog  24939  ang180lem3  24958  basellem2  25228  musumsum  25338  dchrhash  25416  lgsdir2lem5  25474  rpvmasumlem  25596  rpvmasum2  25621  pntlemj  25712  tgcolg  25873  tgbtwnconn1  25894  tgbtwnconn2  25895  hlid  25928  hltr  25929  hlbtwn  25930  lnhl  25934  colmid  26007  hlpasch  26072  lmieu  26100  lmiinv  26108  cgrahl  26142  cgracol  26143  inaghl  26156  edglnl  26449  umgrvad2edg  26516  nbgrnvtx0  26643  clwlkclwwlklem2a  27334  clwwlknnn  27378  clwwlknfi  27391  clwwlknon1nloop  27470  eupth2lem2  27592  frgrwopreg  27700  2wspmdisj  27714  frgrreg  27805  ex-natded5.7  27822  ex-natded5.13  27826  ex-natded9.20  27828  ex-natded9.20-2  27829  aevdemo  27871  f1ocnt  30102  esumsnf  30667  meascnbl  30823  signsplypnf  31170  signstfvn  31189  hashreprin  31243  circlemeth  31263  sltres  32349  dfrdg4  32592  outsideoftr  32770  lineunray  32788  lindsdom  33946  ftc1anclem3  34029  dvasin  34038  areacirclem4  34045  smprngopr  34392  tsbi1  34479  tsbi2  34480  lkrshpor  35181  cdleme22b  36415  tendoex  37049  lcfrlem9  37624  pell1234qrdich  38268  acongtr  38387  acongrep  38389  jm2.23  38405  jm2.25  38408  fnwe2lem3  38464  kelac2lem  38476  ifpim23g  38681  frege122d  38892  clsk1indlem3  39180  refsum2cnlem1  40013  eliuniincex  40106  eliincex  40107  fmul01lt1lem1  40609  limciccioolb  40646  sumnnodd  40655  limcicciooub  40662  wallispilem3  41076  fourierdlem35  41151  fourierdlem80  41195  fourierdlem101  41216  fourierswlem  41239  etransclem32  41275  etransclem35  41278  nnfoctbdjlem  41461  2reu4a  42012  otiunsndisjX  42180  nltle2tri  42209  icceuelpartlem  42257  lighneallem3  42372  evennodd  42404  oddneven  42405  isomuspgrlem1  42563  altgsumbcALT  42996  lindslinindsimp1  43111  lindszr  43123  zlmodzxznm  43151  elfzolborelfzop1  43174  blen1b  43247  reorelicc  43294