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  3465  dcun  3601  exmidn0m  4285  exmidsssn  4286  reg2exmidlema  4626  acexmidlem1  5997  poxp  6378  nntri2or2  6644  nnm00  6676  ssfilem  7037  diffitest  7049  tridc  7061  finexdc  7064  fientri3  7077  unsnfidcex  7082  unsnfidcel  7083  fidcenumlemrks  7120  nninfisollem0  7297  nninfisollemeq  7299  finomni  7307  pr1or2  7367  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidaclem  7390  exmidontriimlem2  7404  netap  7440  2omotaplemap  7443  nqprloc  7732  mullocprlem  7757  recexprlemloc  7818  ltxrlt  8212  zmulcl  9500  nn0lt2  9528  zeo  9552  xrltso  9992  xnn0dcle  9998  xnn0letri  9999  apbtwnz  10494  expnegap0  10769  fzowrddc  11179  xrmaxadd  11772  zsumdc  11895  fsumsplit  11918  sumsplitdc  11943  isumlessdc  12007  zproddc  12090  fprodsplitdc  12107  fprodsplit  12108  fprodunsn  12115  fprodcl2lem  12116  prm23ge5  12787  pcxqcl  12835  gsum0g  13429  lringuplu  14160  suplociccreex  15298  lgsdir2lem5  15711  usgredg2v  16022  djulclALT  16165  trilpolemres  16410  trirec0  16412  nconstwlpolem0  16431  nconstwlpolem  16433