Theorem orcd 740

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

Syntax hints:   -> wi 4   \/ wo 715

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  741  pm2.47  747  orim12i  766  animorl  830  animorrl  833  dcor  943  dfifp2dc  989  undif3ss  3468  dcun  3604  rabsnifsb  3737  exmidn0m  4291  exmidsssn  4292  reg2exmidlema  4632  acexmidlem1  6013  poxp  6396  nntri2or2  6665  nnm00  6697  ssfilem  7061  ssfilemd  7063  diffitest  7075  tridc  7088  finexdc  7091  elssdc  7093  fientri3  7106  unsnfidcex  7111  unsnfidcel  7112  fidcenumlemrks  7151  nninfisollem0  7328  nninfisollemeq  7330  finomni  7338  pr1or2  7398  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  exmidontriimlem2  7436  netap  7472  2omotaplemap  7475  nqprloc  7764  mullocprlem  7789  recexprlemloc  7850  ltxrlt  8244  zmulcl  9532  nn0lt2  9560  zeo  9584  xrltso  10030  xnn0dcle  10036  xnn0letri  10037  apbtwnz  10533  expnegap0  10808  fzowrddc  11227  xrmaxadd  11821  zsumdc  11944  fsumsplit  11967  sumsplitdc  11992  isumlessdc  12056  zproddc  12139  fprodsplitdc  12156  fprodsplit  12157  fprodunsn  12164  fprodcl2lem  12165  prm23ge5  12836  pcxqcl  12884  gsum0g  13478  lringuplu  14209  suplociccreex  15347  lgsdir2lem5  15760  usgredg2v  16074  djulclALT  16397  trilpolemres  16646  trirec0  16648  nconstwlpolem0  16667  nconstwlpolem  16669