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  3425  dcun  3561  exmidn0m  4235  exmidsssn  4236  reg2exmidlema  4571  acexmidlem1  5921  poxp  6299  nntri2or2  6565  nnm00  6597  ssfilem  6945  diffitest  6957  tridc  6969  finexdc  6972  fientri3  6985  unsnfidcex  6990  unsnfidcel  6991  fidcenumlemrks  7028  nninfisollem0  7205  nninfisollemeq  7207  finomni  7215  exmidfodomrlemeldju  7280  exmidfodomrlemreseldju  7281  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidaclem  7293  exmidontriimlem2  7307  netap  7339  2omotaplemap  7342  nqprloc  7631  mullocprlem  7656  recexprlemloc  7717  ltxrlt  8111  zmulcl  9398  nn0lt2  9426  zeo  9450  xrltso  9890  xnn0dcle  9896  xnn0letri  9897  apbtwnz  10383  expnegap0  10658  xrmaxadd  11445  zsumdc  11568  fsumsplit  11591  sumsplitdc  11616  isumlessdc  11680  zproddc  11763  fprodsplitdc  11780  fprodsplit  11781  fprodunsn  11788  fprodcl2lem  11789  prm23ge5  12460  pcxqcl  12508  gsum0g  13100  lringuplu  13830  suplociccreex  14968  lgsdir2lem5  15381  djulclALT  15555  trilpolemres  15799  trirec0  15801  nconstwlpolem0  15820  nconstwlpolem  15822