Theorem olcd 735

Description: Deduction introducing a disjunct. (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 734	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
3	2	orcomd 730	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  742  pm2.49  743  orim12i  760  pm1.5  766  animorr  825  animorlr  826  dcor  937  dcfrompeirce  1460  dcun  3561  exmidn0m  4235  regexmidlem1  4570  reg2exmidlema  4571  nn0suc  4641  nndceq0  4655  acexmidlem1  5921  nntri3or  6560  nntri2or2  6565  nndceq  6566  nndcel  6567  nnm00  6597  ssfilem  6945  diffitest  6957  tridc  6969  finexdc  6972  fientri3  6985  unsnfidcex  6990  unsnfidcel  6991  fidcenumlemrks  7028  fidcenumlemrk  7029  nninfisollemne  7206  nninfisol  7208  finomni  7215  exmidfodomrlemeldju  7280  exmidfodomrlemreseldju  7281  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidaclem  7293  exmidontriimlem2  7307  netap  7339  2omotaplemap  7342  mullocprlem  7656  recexprlemloc  7717  gt0ap0  8672  ltap  8679  recexaplem2  8698  nn1m1nn  9027  nn1gt1  9043  ltpnf  9874  mnflt  9877  xrltso  9890  xnn0dcle  9896  xnn0letri  9897  xrpnfdc  9936  xrmnfdc  9937  exfzdc  10335  infssuzex  10342  apbtwnz  10383  expnnval  10653  exp0  10654  bc0k  10867  bcpasc  10877  xrmaxadd  11445  sumdc  11542  zsumdc  11568  fsum3  11571  fisumss  11576  isumss2  11577  fsumsplit  11591  zproddc  11763  fprodseq  11767  fprodssdc  11774  fprodsplitdc  11780  fprodsplit  11781  fprodunsn  11788  fprodcl2lem  11789  fsumdvds  12026  pclemdc  12484  pcxqcl  12508  sumhashdc  12543  1arith  12563  4sqlem17  12603  ctiunctlemudc  12681  lringuplu  13830  suplociccreex  14968  plymullem1  15092  lgsdir2lem5  15381  djurclALT  15556  bj-nn0suc0  15704  trilpolemres  15799  trirec0  15801  nconstwlpolem  15822