Theorem olcd 652

Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
orcd.1	|- (ph -> ps)

Assertion

Ref	Expression
olcd	|- (ph -> (ch \/ ps))

Proof of Theorem olcd

Step	Hyp	Ref	Expression
1		orcd.1	. . 3 |- (ph -> ps)
2	1	orcd 651	. 2 |- (ph -> (ps \/ ch))
3	2	orcomd 647	1 |- (ph -> (ch \/ ps))

Syntax hints:   -> wi 4   \/ wo 628

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.48  659  pm2.49  660  orim12i  675  pm1.5  681  dcan  841  dcor  842  sspsstrir  3040  regexmidlem1  4218  nn0suc  4270  nndceq0  4282  acexmidlem1  5451  nntri3or  6011  nndceq  6015  nndcel  6016  nnm00  6038  ssfiexmid  6254  mullocprlem  6551  recexprlemloc  6603  gt0ap0  7408  recexaplem2  7415  nn1m1nn  7713  nn1gt1  7728  ltpnf  8472  mnflt  8474  xrltso  8487  expinnval  8912  exp0  8913  bj-nn0suc0  9410