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  3531  exmidn0m  4196  regexmidlem1  4526  reg2exmidlema  4527  nn0suc  4597  nndceq0  4611  acexmidlem1  5861  nntri3or  6484  nntri2or2  6489  nndceq  6490  nndcel  6491  nnm00  6521  ssfilem  6865  diffitest  6877  tridc  6889  finexdc  6892  fientri3  6904  unsnfidcex  6909  unsnfidcel  6910  fidcenumlemrks  6942  fidcenumlemrk  6943  nninfisollemne  7119  nninfisol  7121  finomni  7128  exmidfodomrlemeldju  7188  exmidfodomrlemreseldju  7189  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  exmidaclem  7197  exmidontriimlem2  7211  mullocprlem  7544  recexprlemloc  7605  gt0ap0  8557  ltap  8564  recexaplem2  8582  nn1m1nn  8908  nn1gt1  8924  ltpnf  9749  mnflt  9752  xrltso  9765  xnn0dcle  9771  xnn0letri  9772  xrpnfdc  9811  xrmnfdc  9812  exfzdc  10208  apbtwnz  10242  expnnval  10491  exp0  10492  bc0k  10702  bcpasc  10712  xrmaxadd  11235  sumdc  11332  zsumdc  11358  fsum3  11361  fisumss  11366  isumss2  11367  fsumsplit  11381  zproddc  11553  fprodseq  11557  fprodssdc  11564  fprodsplitdc  11570  fprodsplit  11571  fprodunsn  11578  fprodcl2lem  11579  infssuzex  11915  pclemdc  12253  sumhashdc  12310  1arith  12330  ctiunctlemudc  12403  suplociccreex  13653  lgsdir2lem5  13984  djurclALT  14094  bj-nn0suc0  14242  trilpolemres  14331  trirec0  14333  nconstwlpolem  14353