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  3434  dcun  3570  exmidn0m  4245  exmidsssn  4246  reg2exmidlema  4582  acexmidlem1  5940  poxp  6318  nntri2or2  6584  nnm00  6616  ssfilem  6972  diffitest  6984  tridc  6996  finexdc  6999  fientri3  7012  unsnfidcex  7017  unsnfidcel  7018  fidcenumlemrks  7055  nninfisollem0  7232  nninfisollemeq  7234  finomni  7242  exmidfodomrlemeldju  7307  exmidfodomrlemreseldju  7308  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidaclem  7320  exmidontriimlem2  7334  netap  7366  2omotaplemap  7369  nqprloc  7658  mullocprlem  7683  recexprlemloc  7744  ltxrlt  8138  zmulcl  9426  nn0lt2  9454  zeo  9478  xrltso  9918  xnn0dcle  9924  xnn0letri  9925  apbtwnz  10417  expnegap0  10692  fzowrddc  11100  xrmaxadd  11572  zsumdc  11695  fsumsplit  11718  sumsplitdc  11743  isumlessdc  11807  zproddc  11890  fprodsplitdc  11907  fprodsplit  11908  fprodunsn  11915  fprodcl2lem  11916  prm23ge5  12587  pcxqcl  12635  gsum0g  13228  lringuplu  13958  suplociccreex  15096  lgsdir2lem5  15509  djulclALT  15737  trilpolemres  15981  trirec0  15983  nconstwlpolem0  16002  nconstwlpolem  16004