Theorem olcd 723

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

Syntax hints:   -> wi 4   \/ wo 697

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 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.48  730  pm2.49  731  orim12i  748  pm1.5  754  dcan  918  dcor  919  dcun  3473  exmidn0m  4124  regexmidlem1  4448  reg2exmidlema  4449  nn0suc  4518  nndceq0  4531  acexmidlem1  5770  nntri3or  6389  nntri2or2  6394  nndceq  6395  nndcel  6396  nnm00  6425  ssfilem  6769  diffitest  6781  tridc  6793  finexdc  6796  fientri3  6803  unsnfidcex  6808  unsnfidcel  6809  fidcenumlemrks  6841  fidcenumlemrk  6842  finomni  7012  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  mullocprlem  7378  recexprlemloc  7439  gt0ap0  8388  ltap  8395  recexaplem2  8413  nn1m1nn  8738  nn1gt1  8754  ltpnf  9567  mnflt  9569  xrltso  9582  xrpnfdc  9625  xrmnfdc  9626  exfzdc  10017  apbtwnz  10047  expnnval  10296  exp0  10297  bc0k  10502  bcpasc  10512  xrmaxadd  11030  sumdc  11127  zsumdc  11153  fsum3  11156  fisumss  11161  isumss2  11162  fsumsplit  11176  infssuzex  11642  ctiunctlemudc  11950  suplociccreex  12771  djurclALT  13009  bj-nn0suc0  13148  trilpolemres  13235