Theorem olcd 741

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

Syntax hints:   -> wi 4   \/ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  748  pm2.49  749  orim12i  766  pm1.5  772  animorr  831  animorlr  832  dcor  943  dfifp2dc  989  dcfrompeirce  1494  dcun  3604  exmidn0m  4291  regexmidlem1  4631  reg2exmidlema  4632  nn0suc  4702  nndceq0  4716  acexmidlem1  6014  nntri3or  6661  nntri2or2  6666  nndceq  6667  nndcel  6668  nnm00  6698  ssfilem  7062  ssfilemd  7064  diffitest  7076  tridc  7089  finexdc  7092  elssdc  7094  eqsndc  7095  fientri3  7107  unsnfidcex  7112  unsnfidcel  7113  fidcenumlemrks  7152  fidcenumlemrk  7153  nninfisollemne  7330  nninfisol  7332  finomni  7339  pr1or2  7399  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  exmidontriimlem2  7437  netap  7473  2omotaplemap  7476  mullocprlem  7790  recexprlemloc  7851  gt0ap0  8806  ltap  8813  recexaplem2  8832  nn1m1nn  9161  nn1gt1  9177  ltpnf  10015  mnflt  10018  xrltso  10031  xnn0dcle  10037  xnn0letri  10038  xrpnfdc  10077  xrmnfdc  10078  exfzdc  10487  infssuzex  10494  apbtwnz  10535  expnnval  10805  exp0  10806  bc0k  11019  bcpasc  11029  ccatsymb  11183  xrmaxadd  11839  sumdc  11936  zsumdc  11963  fsum3  11966  fisumss  11971  isumss2  11972  fsumsplit  11986  zproddc  12158  fprodseq  12162  fprodssdc  12169  fprodsplitdc  12175  fprodsplit  12176  fprodunsn  12183  fprodcl2lem  12184  fsumdvds  12421  pclemdc  12879  pcxqcl  12903  sumhashdc  12938  1arith  12958  4sqlem17  12998  ctiunctlemudc  13076  lringuplu  14229  suplociccreex  15367  plymullem1  15491  lgsdir2lem5  15780  upgr1een  15994  umgrvad2edg  16081  usgr1e  16111  eupth2lem2dc  16329  eupth2lem3lem4fi  16343  djurclALT  16449  bj-nn0suc0  16596  trilpolemres  16697  trirec0  16699  nconstwlpolem  16721