Theorem orcd 735

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

Syntax hints:   -> wi 4   \/ wo 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  736  pm2.47  742  orim12i  761  animorl  825  animorrl  828  dcor  938  undif3ss  3442  dcun  3578  exmidn0m  4261  exmidsssn  4262  reg2exmidlema  4600  acexmidlem1  5963  poxp  6341  nntri2or2  6607  nnm00  6639  ssfilem  6998  diffitest  7010  tridc  7022  finexdc  7025  fientri3  7038  unsnfidcex  7043  unsnfidcel  7044  fidcenumlemrks  7081  nninfisollem0  7258  nninfisollemeq  7260  finomni  7268  pr1or2  7328  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidaclem  7351  exmidontriimlem2  7365  netap  7401  2omotaplemap  7404  nqprloc  7693  mullocprlem  7718  recexprlemloc  7779  ltxrlt  8173  zmulcl  9461  nn0lt2  9489  zeo  9513  xrltso  9953  xnn0dcle  9959  xnn0letri  9960  apbtwnz  10454  expnegap0  10729  fzowrddc  11138  xrmaxadd  11687  zsumdc  11810  fsumsplit  11833  sumsplitdc  11858  isumlessdc  11922  zproddc  12005  fprodsplitdc  12022  fprodsplit  12023  fprodunsn  12030  fprodcl2lem  12031  prm23ge5  12702  pcxqcl  12750  gsum0g  13343  lringuplu  14073  suplociccreex  15211  lgsdir2lem5  15624  djulclALT  15937  trilpolemres  16183  trirec0  16185  nconstwlpolem0  16204  nconstwlpolem  16206