Theorem olcd 734

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 733	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
3	2	orcomd 729	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  741  pm2.49  742  orim12i  759  pm1.5  765  animorr  824  animorlr  825  dcan  933  dcor  935  dcun  3533  exmidn0m  4201  regexmidlem1  4532  reg2exmidlema  4533  nn0suc  4603  nndceq0  4617  acexmidlem1  5870  nntri3or  6493  nntri2or2  6498  nndceq  6499  nndcel  6500  nnm00  6530  ssfilem  6874  diffitest  6886  tridc  6898  finexdc  6901  fientri3  6913  unsnfidcex  6918  unsnfidcel  6919  fidcenumlemrks  6951  fidcenumlemrk  6952  nninfisollemne  7128  nninfisol  7130  finomni  7137  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  exmidontriimlem2  7220  netap  7252  2omotaplemap  7255  mullocprlem  7568  recexprlemloc  7629  gt0ap0  8582  ltap  8589  recexaplem2  8608  nn1m1nn  8936  nn1gt1  8952  ltpnf  9779  mnflt  9782  xrltso  9795  xnn0dcle  9801  xnn0letri  9802  xrpnfdc  9841  xrmnfdc  9842  exfzdc  10239  apbtwnz  10273  expnnval  10522  exp0  10523  bc0k  10735  bcpasc  10745  xrmaxadd  11268  sumdc  11365  zsumdc  11391  fsum3  11394  fisumss  11399  isumss2  11400  fsumsplit  11414  zproddc  11586  fprodseq  11590  fprodssdc  11597  fprodsplitdc  11603  fprodsplit  11604  fprodunsn  11611  fprodcl2lem  11612  infssuzex  11949  pclemdc  12287  sumhashdc  12344  1arith  12364  ctiunctlemudc  12437  lringuplu  13335  suplociccreex  14072  lgsdir2lem5  14403  djurclALT  14524  bj-nn0suc0  14672  trilpolemres  14760  trirec0  14762  nconstwlpolem  14782