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  4199  regexmidlem1  4530  reg2exmidlema  4531  nn0suc  4601  nndceq0  4615  acexmidlem1  5866  nntri3or  6489  nntri2or2  6494  nndceq  6495  nndcel  6496  nnm00  6526  ssfilem  6870  diffitest  6882  tridc  6894  finexdc  6897  fientri3  6909  unsnfidcex  6914  unsnfidcel  6915  fidcenumlemrks  6947  fidcenumlemrk  6948  nninfisollemne  7124  nninfisol  7126  finomni  7133  exmidfodomrlemeldju  7193  exmidfodomrlemreseldju  7194  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidaclem  7202  exmidontriimlem2  7216  netap  7248  2omotaplemap  7251  mullocprlem  7564  recexprlemloc  7625  gt0ap0  8577  ltap  8584  recexaplem2  8603  nn1m1nn  8931  nn1gt1  8947  ltpnf  9774  mnflt  9777  xrltso  9790  xnn0dcle  9796  xnn0letri  9797  xrpnfdc  9836  xrmnfdc  9837  exfzdc  10233  apbtwnz  10267  expnnval  10516  exp0  10517  bc0k  10727  bcpasc  10737  xrmaxadd  11260  sumdc  11357  zsumdc  11383  fsum3  11386  fisumss  11391  isumss2  11392  fsumsplit  11406  zproddc  11578  fprodseq  11582  fprodssdc  11589  fprodsplitdc  11595  fprodsplit  11596  fprodunsn  11603  fprodcl2lem  11604  infssuzex  11940  pclemdc  12278  sumhashdc  12335  1arith  12355  ctiunctlemudc  12428  lringuplu  13236  suplociccreex  13884  lgsdir2lem5  14215  djurclALT  14325  bj-nn0suc0  14473  trilpolemres  14561  trirec0  14563  nconstwlpolem  14583