Theorem olcd 729

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

Syntax hints:   → wi 4   ∨ wo 703

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.48  736  pm2.49  737  orim12i  754  pm1.5  760  animorr  819  animorlr  820  dcan  928  dcor  930  dcun  3525  exmidn0m  4187  regexmidlem1  4517  reg2exmidlema  4518  nn0suc  4588  nndceq0  4602  acexmidlem1  5849  nntri3or  6472  nntri2or2  6477  nndceq  6478  nndcel  6479  nnm00  6509  ssfilem  6853  diffitest  6865  tridc  6877  finexdc  6880  fientri3  6892  unsnfidcex  6897  unsnfidcel  6898  fidcenumlemrks  6930  fidcenumlemrk  6931  nninfisollemne  7107  nninfisol  7109  finomni  7116  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  exmidontriimlem2  7199  mullocprlem  7532  recexprlemloc  7593  gt0ap0  8545  ltap  8552  recexaplem2  8570  nn1m1nn  8896  nn1gt1  8912  ltpnf  9737  mnflt  9740  xrltso  9753  xnn0dcle  9759  xnn0letri  9760  xrpnfdc  9799  xrmnfdc  9800  exfzdc  10196  apbtwnz  10230  expnnval  10479  exp0  10480  bc0k  10690  bcpasc  10700  xrmaxadd  11224  sumdc  11321  zsumdc  11347  fsum3  11350  fisumss  11355  isumss2  11356  fsumsplit  11370  zproddc  11542  fprodseq  11546  fprodssdc  11553  fprodsplitdc  11559  fprodsplit  11560  fprodunsn  11567  fprodcl2lem  11568  infssuzex  11904  pclemdc  12242  sumhashdc  12299  1arith  12319  ctiunctlemudc  12392  suplociccreex  13396  lgsdir2lem5  13727  djurclALT  13837  bj-nn0suc0  13985  trilpolemres  14074  trirec0  14076  nconstwlpolem  14096