Theorem olcd 653

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 652	. 2 |- ( ph -> ( ps \/ ch ) )
3	2	orcomd 648	1 |- ( ph -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 629

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 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.48  660  pm2.49  661  orim12i  676  pm1.5  682  dcan  842  dcor  843  sspsstrir  3046  regexmidlem1  4258  reg2exmidlema  4259  nn0suc  4327  nndceq0  4339  acexmidlem1  5508  nntri3or  6072  nntri2or2  6076  nndceq  6077  nndcel  6078  nnm00  6102  ssfiexmid  6336  diffitest  6344  fientri3  6353  mullocprlem  6668  recexprlemloc  6729  gt0ap0  7616  ltap  7622  recexaplem2  7633  nn1m1nn  7932  nn1gt1  7947  ltpnf  8702  mnflt  8704  xrltso  8717  expinnval  9258  exp0  9259  bj-nn0suc0  10075