Theorem olcd 736

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

Syntax hints:   -> wi 4   \/ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  743  pm2.49  744  orim12i  761  pm1.5  767  animorr  826  animorlr  827  dcor  938  dcfrompeirce  1470  dcun  3578  exmidn0m  4261  regexmidlem1  4599  reg2exmidlema  4600  nn0suc  4670  nndceq0  4684  acexmidlem1  5963  nntri3or  6602  nntri2or2  6607  nndceq  6608  nndcel  6609  nnm00  6639  ssfilem  6998  diffitest  7010  tridc  7022  finexdc  7025  fientri3  7038  unsnfidcex  7043  unsnfidcel  7044  fidcenumlemrks  7081  fidcenumlemrk  7082  nninfisollemne  7259  nninfisol  7261  finomni  7268  pr1or2  7328  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidaclem  7351  exmidontriimlem2  7365  netap  7401  2omotaplemap  7404  mullocprlem  7718  recexprlemloc  7779  gt0ap0  8734  ltap  8741  recexaplem2  8760  nn1m1nn  9089  nn1gt1  9105  ltpnf  9937  mnflt  9940  xrltso  9953  xnn0dcle  9959  xnn0letri  9960  xrpnfdc  9999  xrmnfdc  10000  exfzdc  10406  infssuzex  10413  apbtwnz  10454  expnnval  10724  exp0  10725  bc0k  10938  bcpasc  10948  ccatsymb  11096  xrmaxadd  11687  sumdc  11784  zsumdc  11810  fsum3  11813  fisumss  11818  isumss2  11819  fsumsplit  11833  zproddc  12005  fprodseq  12009  fprodssdc  12016  fprodsplitdc  12022  fprodsplit  12023  fprodunsn  12030  fprodcl2lem  12031  fsumdvds  12268  pclemdc  12726  pcxqcl  12750  sumhashdc  12785  1arith  12805  4sqlem17  12845  ctiunctlemudc  12923  lringuplu  14073  suplociccreex  15211  plymullem1  15335  lgsdir2lem5  15624  djurclALT  15938  bj-nn0suc0  16085  trilpolemres  16183  trirec0  16185  nconstwlpolem  16206