Theorem orcd 741

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

Syntax hints:   -> wi 4   \/ wo 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  742  pm2.47  748  orim12i  767  animorl  831  animorrl  834  dcor  944  dfifp2dc  990  undif3ss  3470  dcun  3606  rabsnifsb  3741  exmidn0m  4297  exmidsssn  4298  reg2exmidlema  4638  acexmidlem1  6024  poxp  6406  nntri2or2  6709  nnm00  6741  ssfilem  7105  ssfilemd  7107  diffitest  7119  tridc  7132  finexdc  7135  elssdc  7137  fientri3  7150  unsnfidcex  7155  unsnfidcel  7156  fidcenumlemrks  7195  nninfisollem0  7389  nninfisollemeq  7391  finomni  7399  pr1or2  7459  exmidfodomrlemeldju  7470  exmidfodomrlemreseldju  7471  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidaclem  7483  exmidontriimlem2  7497  netap  7533  2omotaplemap  7536  nqprloc  7825  mullocprlem  7850  recexprlemloc  7911  ltxrlt  8304  zmulcl  9594  nn0lt2  9622  zeo  9646  xrltso  10092  xnn0dcle  10098  xnn0letri  10099  apbtwnz  10597  expnegap0  10872  fzowrddc  11294  xrmaxadd  11901  zsumdc  12025  fsumsplit  12048  sumsplitdc  12073  isumlessdc  12137  zproddc  12220  fprodsplitdc  12237  fprodsplit  12238  fprodunsn  12245  fprodcl2lem  12246  prm23ge5  12917  pcxqcl  12965  gsum0g  13559  lringuplu  14291  suplociccreex  15435  lgsdir2lem5  15851  usgredg2v  16165  djulclALT  16519  trilpolemres  16774  trirec0  16776  nconstwlpolem0  16796  nconstwlpolem  16798