Theorem orcd 738

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

Syntax hints:   -> wi 4   \/ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  739  pm2.47  745  orim12i  764  animorl  828  animorrl  831  dcor  941  dfifp2dc  987  undif3ss  3466  dcun  3602  rabsnifsb  3735  exmidn0m  4289  exmidsssn  4290  reg2exmidlema  4630  acexmidlem1  6009  poxp  6392  nntri2or2  6661  nnm00  6693  ssfilem  7057  diffitest  7069  tridc  7082  finexdc  7085  elssdc  7087  fientri3  7100  unsnfidcex  7105  unsnfidcel  7106  fidcenumlemrks  7143  nninfisollem0  7320  nninfisollemeq  7322  finomni  7330  pr1or2  7390  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  exmidontriimlem2  7427  netap  7463  2omotaplemap  7466  nqprloc  7755  mullocprlem  7780  recexprlemloc  7841  ltxrlt  8235  zmulcl  9523  nn0lt2  9551  zeo  9575  xrltso  10021  xnn0dcle  10027  xnn0letri  10028  apbtwnz  10524  expnegap0  10799  fzowrddc  11218  xrmaxadd  11812  zsumdc  11935  fsumsplit  11958  sumsplitdc  11983  isumlessdc  12047  zproddc  12130  fprodsplitdc  12147  fprodsplit  12148  fprodunsn  12155  fprodcl2lem  12156  prm23ge5  12827  pcxqcl  12875  gsum0g  13469  lringuplu  14200  suplociccreex  15338  lgsdir2lem5  15751  usgredg2v  16063  djulclALT  16333  trilpolemres  16582  trirec0  16584  nconstwlpolem0  16603  nconstwlpolem  16605