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  dcun  3557  exmidn0m  4231  regexmidlem1  4566  reg2exmidlema  4567  nn0suc  4637  nndceq0  4651  acexmidlem1  5915  nntri3or  6548  nntri2or2  6553  nndceq  6554  nndcel  6555  nnm00  6585  ssfilem  6933  diffitest  6945  tridc  6957  finexdc  6960  fientri3  6973  unsnfidcex  6978  unsnfidcel  6979  fidcenumlemrks  7014  fidcenumlemrk  7015  nninfisollemne  7192  nninfisol  7194  finomni  7201  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  exmidontriimlem2  7284  netap  7316  2omotaplemap  7319  mullocprlem  7632  recexprlemloc  7693  gt0ap0  8647  ltap  8654  recexaplem2  8673  nn1m1nn  9002  nn1gt1  9018  ltpnf  9849  mnflt  9852  xrltso  9865  xnn0dcle  9871  xnn0letri  9872  xrpnfdc  9911  xrmnfdc  9912  exfzdc  10310  apbtwnz  10346  expnnval  10616  exp0  10617  bc0k  10830  bcpasc  10840  xrmaxadd  11407  sumdc  11504  zsumdc  11530  fsum3  11533  fisumss  11538  isumss2  11539  fsumsplit  11553  zproddc  11725  fprodseq  11729  fprodssdc  11736  fprodsplitdc  11742  fprodsplit  11743  fprodunsn  11750  fprodcl2lem  11751  infssuzex  12089  pclemdc  12429  pcxqcl  12453  sumhashdc  12488  1arith  12508  4sqlem17  12548  ctiunctlemudc  12597  lringuplu  13695  suplociccreex  14803  plymullem1  14927  lgsdir2lem5  15189  djurclALT  15364  bj-nn0suc0  15512  trilpolemres  15602  trirec0  15604  nconstwlpolem  15625