Theorem orcd 735

Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)

Hypothesis

Ref	Expression
orcd.1	|- ( ph -> ps )

Assertion

Ref	Expression
orcd	|- ( ph -> ( ps \/ ch ) )

Proof of Theorem orcd

Step	Hyp	Ref	Expression
1		orcd.1	. 2 |- ( ph -> ps )
2		orc 714	. 2 |- ( ps -> ( ps \/ ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps \/ ch ) )

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-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  736  pm2.47  742  orim12i  761  animorl  825  animorrl  828  dcor  938  undif3ss  3434  dcun  3570  exmidn0m  4246  exmidsssn  4247  reg2exmidlema  4583  acexmidlem1  5942  poxp  6320  nntri2or2  6586  nnm00  6618  ssfilem  6974  diffitest  6986  tridc  6998  finexdc  7001  fientri3  7014  unsnfidcex  7019  unsnfidcel  7020  fidcenumlemrks  7057  nninfisollem0  7234  nninfisollemeq  7236  finomni  7244  exmidfodomrlemeldju  7309  exmidfodomrlemreseldju  7310  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidaclem  7322  exmidontriimlem2  7336  netap  7368  2omotaplemap  7371  nqprloc  7660  mullocprlem  7685  recexprlemloc  7746  ltxrlt  8140  zmulcl  9428  nn0lt2  9456  zeo  9480  xrltso  9920  xnn0dcle  9926  xnn0letri  9927  apbtwnz  10419  expnegap0  10694  fzowrddc  11103  xrmaxadd  11605  zsumdc  11728  fsumsplit  11751  sumsplitdc  11776  isumlessdc  11840  zproddc  11923  fprodsplitdc  11940  fprodsplit  11941  fprodunsn  11948  fprodcl2lem  11949  prm23ge5  12620  pcxqcl  12668  gsum0g  13261  lringuplu  13991  suplociccreex  15129  lgsdir2lem5  15542  djulclALT  15774  trilpolemres  16018  trirec0  16020  nconstwlpolem0  16039  nconstwlpolem  16041