Theorem orcd 723

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 702	. 2 |- ( ps -> ( ps \/ ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps \/ ch ) )

Syntax hints:   -> wi 4   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  724  pm2.47  730  orim12i  749  dcor  920  undif3ss  3368  dcun  3504  exmidn0m  4161  exmidsssn  4162  reg2exmidlema  4491  acexmidlem1  5814  poxp  6173  nntri2or2  6438  nnm00  6469  ssfilem  6813  diffitest  6825  tridc  6837  finexdc  6840  fientri3  6852  unsnfidcex  6857  unsnfidcel  6858  fidcenumlemrks  6890  finomni  7066  exmidfodomrlemeldju  7117  exmidfodomrlemreseldju  7118  exmidfodomrlemr  7120  exmidfodomrlemrALT  7121  exmidaclem  7126  exmidontriimlem2  7140  nqprloc  7448  mullocprlem  7473  recexprlemloc  7534  ltxrlt  7926  zmulcl  9203  nn0lt2  9228  zeo  9252  xrltso  9685  apbtwnz  10155  expnegap0  10409  xrmaxadd  11140  zsumdc  11263  fsumsplit  11286  sumsplitdc  11311  isumlessdc  11375  zproddc  11458  fprodsplitdc  11475  fprodsplit  11476  fprodunsn  11483  fprodcl2lem  11484  suplociccreex  12962  djulclALT  13335  trilpolemres  13576  trirec0  13578  nconstwlpolem0  13596  nconstwlpolem  13598