Theorem olcd 742

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

Syntax hints:   -> wi 4   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  749  pm2.49  750  orim12i  767  pm1.5  773  animorr  832  animorlr  833  dcor  944  dfifp2dc  990  dcfrompeirce  1495  dcun  3623  exmidn0m  4319  regexmidlem1  4660  reg2exmidlema  4661  nn0suc  4731  nndceq0  4745  acexmidlem1  6054  nntri3or  6739  nntri2or2  6744  nndceq  6745  nndcel  6746  nnm00  6776  ssfilem  7143  ssfilemd  7145  diffitest  7157  tridc  7170  finexdc  7173  elssdc  7175  eqsndc  7176  fientri3  7188  unsnfidcex  7193  unsnfidcel  7194  fidcenumlemrks  7236  fidcenumlemrk  7237  nninfisollemne  7435  nninfisol  7437  finomni  7444  pr1or2  7504  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  exmidontriimlem2  7542  netap  7584  2omotaplemap  7587  mullocprlem  7901  recexprlemloc  7962  gt0ap0  8917  ltap  8924  recexaplem2  8943  nn1m1nn  9272  nn1gt1  9288  ltpnf  10132  mnflt  10135  xrltso  10148  xnn0dcle  10154  xnn0letri  10155  xrpnfdc  10194  xrmnfdc  10195  exfzdc  10608  infssuzex  10615  apbtwnz  10658  expnnval  10928  exp0  10929  resq01  11044  bc0k  11143  bcpasc  11153  ccatsymb  11315  xrmaxadd  11971  sumdc  12068  zsumdc  12095  fsum3  12098  fisumss  12103  isumss2  12104  fsumsplit  12118  zproddc  12290  fprodseq  12294  fprodssdc  12301  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  fprodcl2lem  12316  fsumdvds  12553  pclemdc  13011  pcxqcl  13035  sumhashdc  13070  1arith  13090  4sqlem17  13130  ctiunctlemudc  13272  lringuplu  14441  aprlring  14538  suplociccreex  15615  plymullem1  15739  lgsdir2lem5  16031  upgr1een  16245  umgrvad2edg  16332  usgr1e  16362  eupth2lem2dc  16580  eupth2lem3lem4fi  16594  djurclALT  16700  bj-nn0suc0  16846  trilpolemres  16952  trirec0  16954  trimul0or  16971  nconstwlpolem  16977