Theorem olcd 724

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

Syntax hints:   -> wi 4   \/ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.48  731  pm2.49  732  orim12i  749  pm1.5  755  dcan  919  dcor  920  dcun  3478  exmidn0m  4132  regexmidlem1  4456  reg2exmidlema  4457  nn0suc  4526  nndceq0  4539  acexmidlem1  5778  nntri3or  6397  nntri2or2  6402  nndceq  6403  nndcel  6404  nnm00  6433  ssfilem  6777  diffitest  6789  tridc  6801  finexdc  6804  fientri3  6811  unsnfidcex  6816  unsnfidcel  6817  fidcenumlemrks  6849  fidcenumlemrk  6850  finomni  7020  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  mullocprlem  7402  recexprlemloc  7463  gt0ap0  8412  ltap  8419  recexaplem2  8437  nn1m1nn  8762  nn1gt1  8778  ltpnf  9597  mnflt  9599  xrltso  9612  xrpnfdc  9655  xrmnfdc  9656  exfzdc  10048  apbtwnz  10078  expnnval  10327  exp0  10328  bc0k  10534  bcpasc  10544  xrmaxadd  11062  sumdc  11159  zsumdc  11185  fsum3  11188  fisumss  11193  isumss2  11194  fsumsplit  11208  zproddc  11380  fprodseq  11384  infssuzex  11678  ctiunctlemudc  11986  suplociccreex  12810  djurclALT  13180  bj-nn0suc0  13319  trilpolemres  13410  trirec0  13412