Theorem orcd 740

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

Syntax hints:   -> wi 4   \/ wo 715

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  741  pm2.47  747  orim12i  766  animorl  830  animorrl  833  dcor  943  dfifp2dc  989  undif3ss  3468  dcun  3604  rabsnifsb  3737  exmidn0m  4291  exmidsssn  4292  reg2exmidlema  4632  acexmidlem1  6014  poxp  6397  nntri2or2  6666  nnm00  6698  ssfilem  7062  ssfilemd  7064  diffitest  7076  tridc  7089  finexdc  7092  elssdc  7094  fientri3  7107  unsnfidcex  7112  unsnfidcel  7113  fidcenumlemrks  7152  nninfisollem0  7329  nninfisollemeq  7331  finomni  7339  pr1or2  7399  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  exmidontriimlem2  7437  netap  7473  2omotaplemap  7476  nqprloc  7765  mullocprlem  7790  recexprlemloc  7851  ltxrlt  8245  zmulcl  9533  nn0lt2  9561  zeo  9585  xrltso  10031  xnn0dcle  10037  xnn0letri  10038  apbtwnz  10535  expnegap0  10810  fzowrddc  11232  xrmaxadd  11839  zsumdc  11963  fsumsplit  11986  sumsplitdc  12011  isumlessdc  12075  zproddc  12158  fprodsplitdc  12175  fprodsplit  12176  fprodunsn  12183  fprodcl2lem  12184  prm23ge5  12855  pcxqcl  12903  gsum0g  13497  lringuplu  14229  suplociccreex  15367  lgsdir2lem5  15780  usgredg2v  16094  djulclALT  16448  trilpolemres  16697  trirec0  16699  nconstwlpolem0  16719  nconstwlpolem  16721