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  3504  exmidn0m  4162  regexmidlem1  4492  reg2exmidlema  4493  nn0suc  4563  nndceq0  4577  acexmidlem1  5820  nntri3or  6440  nntri2or2  6445  nndceq  6446  nndcel  6447  nnm00  6476  ssfilem  6820  diffitest  6832  tridc  6844  finexdc  6847  fientri3  6859  unsnfidcex  6864  unsnfidcel  6865  fidcenumlemrks  6897  fidcenumlemrk  6898  nninfisollemne  7074  nninfisol  7076  finomni  7083  exmidfodomrlemeldju  7134  exmidfodomrlemreseldju  7135  exmidfodomrlemr  7137  exmidfodomrlemrALT  7138  exmidaclem  7143  exmidontriimlem2  7157  mullocprlem  7490  recexprlemloc  7551  gt0ap0  8501  ltap  8508  recexaplem2  8526  nn1m1nn  8851  nn1gt1  8867  ltpnf  9687  mnflt  9690  xrltso  9703  xrpnfdc  9746  xrmnfdc  9747  exfzdc  10139  apbtwnz  10173  expnnval  10422  exp0  10423  bc0k  10630  bcpasc  10640  xrmaxadd  11158  sumdc  11255  zsumdc  11281  fsum3  11284  fisumss  11289  isumss2  11290  fsumsplit  11304  zproddc  11476  fprodseq  11480  fprodssdc  11487  fprodsplitdc  11493  fprodsplit  11494  fprodunsn  11501  fprodcl2lem  11502  infssuzex  11836  ctiunctlemudc  12177  suplociccreex  13013  djurclALT  13387  bj-nn0suc0  13536  trilpolemres  13624  trirec0  13626  nconstwlpolem  13646