Theorem olcd 408

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

Syntax hints:   → wi 4   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  pm2.48  415  pm2.49  416  animorr  506  animorlr  507  orim12i  538  pm1.5  544  cases2  993  eqoreldifOLD  4226  n0snor2el  4364  disjord  4641  propeqop  4970  somin1  5529  soxp  7290  fowdom  8476  unxpwdom2  8493  fin1a2lem11  9232  axdc3lem2  9273  gchdomtri  9451  hargch  9495  alephgch  9496  nn1m1nn  11040  nn01to3  11781  rpneg  11863  ltpnf  11954  mnflt  11957  xrlttri  11972  xmulpnf1  12104  iccsplit  12305  elfznelfzo  12573  addmodlteq  12745  bc0k  13098  bcpasc  13108  hashv01gt1  13133  hashrabsn01  13162  hashsn01  13204  hashf1  13241  pr2pwpr  13261  hashtpg  13267  ffz0iswrd  13332  ccatsymb  13366  s3sndisj  13706  s3iunsndisj  13707  fsum  14451  fsumsplit  14471  fprod  14671  binomfallfaclem2  14771  fsumdvds  15030  pwp1fsum  15114  lcmfunsnlem1  15350  lcmfunsnlem2  15353  ncoprmlnprm  15436  sumhash  15600  4sqlem17  15665  vdwlem6  15690  ram0  15726  cshwsidrepswmod0  15801  cshwsdisj  15805  basprssdmsets  15925  mreexfidimd  16311  sgrp2nmndlem5  17416  psgnunilem1  17913  psgnunilem5  17914  gsummulg  18342  srgbinomlem3  18542  drngnidl  19229  gsummoncoe1  19674  cnsubrg  19806  pmatcoe1fsupp  20506  mp2pm2mplem4  20614  en2top  20789  fctop  20808  cctop  20810  metustto  22358  pmltpclem2  23218  itg1addlem5  23467  itg10a  23477  dvne0  23774  plyeq0lem  23966  plymullem1  23970  aalioulem4  24090  aalioulem5  24091  aaliou2b  24096  relogbf  24529  logblog  24530  ang180lem3  24541  basellem2  24808  musumsum  24918  dchrhash  24996  lgsdir2lem5  25054  rpvmasumlem  25176  rpvmasum2  25201  pntlemj  25292  tgcolg  25449  tgbtwnconn1  25470  tgbtwnconn2  25471  hlid  25504  hltr  25505  hlbtwn  25506  lnhl  25510  colmid  25583  hlpasch  25648  lmieu  25676  lmiinv  25684  cgrahl  25718  cgracol  25719  inaghl  25731  edglnl  26038  umgrvad2edg  26105  nbgrnvtx0  26237  clwlkclwwlklem2a  26899  clwwlksnfi  26913  eupth2lem2  27079  frgrwopreg  27187  2wspmdisj  27201  frgrreg  27252  ex-natded5.7  27268  ex-natded5.13  27272  ex-natded9.20  27274  ex-natded9.20-2  27275  aevdemo  27317  f1ocnt  29559  esumsnf  30126  meascnbl  30282  signsplypnf  30627  signstfvn  30646  hashreprin  30698  circlemeth  30718  sltres  31815  dfrdg4  32058  outsideoftr  32236  lineunray  32254  lindsdom  33403  ftc1anclem3  33487  dvasin  33496  areacirclem4  33503  smprngopr  33851  tsbi1  33940  tsbi2  33941  lkrshpor  34394  cdleme22b  35629  tendoex  36263  lcfrlem9  36839  pell1234qrdich  37425  acongtr  37545  acongrep  37547  jm2.23  37563  jm2.25  37566  fnwe2lem3  37622  kelac2lem  37634  ifpim23g  37840  frege122d  38052  clsk1indlem3  38341  refsum2cnlem1  39196  eliuniincex  39292  eliincex  39293  fmul01lt1lem1  39816  limciccioolb  39853  sumnnodd  39862  limcicciooub  39869  wallispilem3  40284  fourierdlem35  40359  fourierdlem80  40403  fourierdlem101  40424  fourierswlem  40447  etransclem32  40483  etransclem35  40486  nnfoctbdjlem  40672  2reu4a  41189  otiunsndisjX  41298  nltle2tri  41323  icceuelpartlem  41371  lighneallem3  41524  evennodd  41556  oddneven  41557  altgsumbcALT  42131  lindslinindsimp1  42246  lindszr  42258  zlmodzxznm  42286  elfzolborelfzop1  42309  blen1b  42382