Theorem orcd 722

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

Syntax hints:   -> wi 4   \/ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  723  pm2.47  729  orim12i  748  dcor  919  undif3ss  3337  dcun  3473  exmidn0m  4124  exmidsssn  4125  reg2exmidlema  4449  acexmidlem1  5770  poxp  6129  nntri2or2  6394  nnm00  6425  ssfilem  6769  diffitest  6781  tridc  6793  finexdc  6796  fientri3  6803  unsnfidcex  6808  unsnfidcel  6809  fidcenumlemrks  6841  finomni  7012  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  nqprloc  7353  mullocprlem  7378  recexprlemloc  7439  ltxrlt  7830  zmulcl  9107  nn0lt2  9132  zeo  9156  xrltso  9582  apbtwnz  10047  expnegap0  10301  xrmaxadd  11030  zsumdc  11153  fsumsplit  11176  sumsplitdc  11201  isumlessdc  11265  suplociccreex  12771  djulclALT  13008  trilpolemres  13235