Theorem olcd 739

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

Syntax hints:   -> wi 4   \/ wo 713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  746  pm2.49  747  orim12i  764  pm1.5  770  animorr  829  animorlr  830  dcor  941  dfifp2dc  987  dcfrompeirce  1492  dcun  3601  exmidn0m  4285  regexmidlem1  4625  reg2exmidlema  4626  nn0suc  4696  nndceq0  4710  acexmidlem1  5997  nntri3or  6639  nntri2or2  6644  nndceq  6645  nndcel  6646  nnm00  6676  ssfilem  7037  diffitest  7049  tridc  7061  finexdc  7064  fientri3  7077  unsnfidcex  7082  unsnfidcel  7083  fidcenumlemrks  7120  fidcenumlemrk  7121  nninfisollemne  7298  nninfisol  7300  finomni  7307  pr1or2  7367  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidaclem  7390  exmidontriimlem2  7404  netap  7440  2omotaplemap  7443  mullocprlem  7757  recexprlemloc  7818  gt0ap0  8773  ltap  8780  recexaplem2  8799  nn1m1nn  9128  nn1gt1  9144  ltpnf  9976  mnflt  9979  xrltso  9992  xnn0dcle  9998  xnn0letri  9999  xrpnfdc  10038  xrmnfdc  10039  exfzdc  10446  infssuzex  10453  apbtwnz  10494  expnnval  10764  exp0  10765  bc0k  10978  bcpasc  10988  ccatsymb  11137  xrmaxadd  11772  sumdc  11869  zsumdc  11895  fsum3  11898  fisumss  11903  isumss2  11904  fsumsplit  11918  zproddc  12090  fprodseq  12094  fprodssdc  12101  fprodsplitdc  12107  fprodsplit  12108  fprodunsn  12115  fprodcl2lem  12116  fsumdvds  12353  pclemdc  12811  pcxqcl  12835  sumhashdc  12870  1arith  12890  4sqlem17  12930  ctiunctlemudc  13008  lringuplu  14160  suplociccreex  15298  plymullem1  15422  lgsdir2lem5  15711  umgrvad2edg  16009  djurclALT  16166  bj-nn0suc0  16313  trilpolemres  16410  trirec0  16412  nconstwlpolem  16433