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  3342  dcun  3478  exmidn0m  4132  exmidsssn  4133  reg2exmidlema  4457  acexmidlem1  5778  poxp  6137  nntri2or2  6402  nnm00  6433  ssfilem  6777  diffitest  6789  tridc  6801  finexdc  6804  fientri3  6811  unsnfidcex  6816  unsnfidcel  6817  fidcenumlemrks  6849  finomni  7020  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  nqprloc  7377  mullocprlem  7402  recexprlemloc  7463  ltxrlt  7854  zmulcl  9131  nn0lt2  9156  zeo  9180  xrltso  9612  apbtwnz  10078  expnegap0  10332  xrmaxadd  11062  zsumdc  11185  fsumsplit  11208  sumsplitdc  11233  isumlessdc  11297  zproddc  11380  suplociccreex  12810  djulclALT  13179  trilpolemres  13410  trirec0  13412