Theorem olcd 735

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

Syntax hints:   -> wi 4   \/ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  742  pm2.49  743  orim12i  760  pm1.5  766  animorr  825  animorlr  826  dcor  937  dcfrompeirce  1460  dcun  3561  exmidn0m  4235  regexmidlem1  4570  reg2exmidlema  4571  nn0suc  4641  nndceq0  4655  acexmidlem1  5919  nntri3or  6553  nntri2or2  6558  nndceq  6559  nndcel  6560  nnm00  6590  ssfilem  6938  diffitest  6950  tridc  6962  finexdc  6965  fientri3  6978  unsnfidcex  6983  unsnfidcel  6984  fidcenumlemrks  7021  fidcenumlemrk  7022  nninfisollemne  7199  nninfisol  7201  finomni  7208  exmidfodomrlemeldju  7269  exmidfodomrlemreseldju  7270  exmidfodomrlemr  7272  exmidfodomrlemrALT  7273  exmidaclem  7278  exmidontriimlem2  7292  netap  7324  2omotaplemap  7327  mullocprlem  7640  recexprlemloc  7701  gt0ap0  8656  ltap  8663  recexaplem2  8682  nn1m1nn  9011  nn1gt1  9027  ltpnf  9858  mnflt  9861  xrltso  9874  xnn0dcle  9880  xnn0letri  9881  xrpnfdc  9920  xrmnfdc  9921  exfzdc  10319  infssuzex  10326  apbtwnz  10367  expnnval  10637  exp0  10638  bc0k  10851  bcpasc  10861  xrmaxadd  11429  sumdc  11526  zsumdc  11552  fsum3  11555  fisumss  11560  isumss2  11561  fsumsplit  11575  zproddc  11747  fprodseq  11751  fprodssdc  11758  fprodsplitdc  11764  fprodsplit  11765  fprodunsn  11772  fprodcl2lem  11773  fsumdvds  12010  pclemdc  12468  pcxqcl  12492  sumhashdc  12527  1arith  12547  4sqlem17  12587  ctiunctlemudc  12665  lringuplu  13778  suplociccreex  14886  plymullem1  15010  lgsdir2lem5  15299  djurclALT  15474  bj-nn0suc0  15622  trilpolemres  15713  trirec0  15715  nconstwlpolem  15736