Theorem olcd 685

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

Syntax hints:   → wi 4   ∨ wo 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.48  692  pm2.49  693  orim12i  708  pm1.5  714  dcan  875  dcor  876  regexmidlem1  4276  reg2exmidlema  4277  nn0suc  4345  nndceq0  4357  acexmidlem1  5528  nntri3or  6095  nntri2or2  6099  nndceq  6100  nndcel  6101  nnm00  6125  ssfilem  6360  diffitest  6371  fientri3  6381  unsnfidcex  6385  unsnfidcel  6386  mullocprlem  6760  recexprlemloc  6821  gt0ap0  7725  ltap  7731  recexaplem2  7742  nn1m1nn  8057  nn1gt1  8072  ltpnf  8856  mnflt  8858  xrltso  8871  exfzdc  9249  expinnval  9479  exp0  9480  bc0k  9683  bcpasc  9693  infssuzex  10345  bj-nn0suc0  10745