Theorem orcd 734

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

Syntax hints:   -> wi 4   \/ wo 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  735  pm2.47  741  orim12i  760  animorl  824  animorrl  827  dcor  937  undif3ss  3421  dcun  3557  exmidn0m  4231  exmidsssn  4232  reg2exmidlema  4567  acexmidlem1  5915  poxp  6287  nntri2or2  6553  nnm00  6585  ssfilem  6933  diffitest  6945  tridc  6957  finexdc  6960  fientri3  6973  unsnfidcex  6978  unsnfidcel  6979  fidcenumlemrks  7014  nninfisollem0  7191  nninfisollemeq  7193  finomni  7201  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  exmidontriimlem2  7284  netap  7316  2omotaplemap  7319  nqprloc  7607  mullocprlem  7632  recexprlemloc  7693  ltxrlt  8087  zmulcl  9373  nn0lt2  9401  zeo  9425  xrltso  9865  xnn0dcle  9871  xnn0letri  9872  apbtwnz  10346  expnegap0  10621  xrmaxadd  11407  zsumdc  11530  fsumsplit  11553  sumsplitdc  11578  isumlessdc  11642  zproddc  11725  fprodsplitdc  11742  fprodsplit  11743  fprodunsn  11750  fprodcl2lem  11751  prm23ge5  12405  pcxqcl  12453  gsum0g  12982  lringuplu  13695  suplociccreex  14803  lgsdir2lem5  15189  djulclALT  15363  trilpolemres  15602  trirec0  15604  nconstwlpolem0  15623  nconstwlpolem  15625