Theorem orcd 733

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

Syntax hints:   -> wi 4   \/ wo 708

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  734  pm2.47  740  orim12i  759  animorl  823  animorrl  826  dcor  935  undif3ss  3397  dcun  3534  exmidn0m  4202  exmidsssn  4203  reg2exmidlema  4534  acexmidlem1  5871  poxp  6233  nntri2or2  6499  nnm00  6531  ssfilem  6875  diffitest  6887  tridc  6899  finexdc  6902  fientri3  6914  unsnfidcex  6919  unsnfidcel  6920  fidcenumlemrks  6952  nninfisollem0  7128  nninfisollemeq  7130  finomni  7138  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  exmidontriimlem2  7221  netap  7253  2omotaplemap  7256  nqprloc  7544  mullocprlem  7569  recexprlemloc  7630  ltxrlt  8023  zmulcl  9306  nn0lt2  9334  zeo  9358  xrltso  9796  xnn0dcle  9802  xnn0letri  9803  apbtwnz  10274  expnegap0  10528  xrmaxadd  11269  zsumdc  11392  fsumsplit  11415  sumsplitdc  11440  isumlessdc  11504  zproddc  11587  fprodsplitdc  11604  fprodsplit  11605  fprodunsn  11612  fprodcl2lem  11613  prm23ge5  12264  lringuplu  13337  suplociccreex  14105  lgsdir2lem5  14436  djulclALT  14556  trilpolemres  14793  trirec0  14795  nconstwlpolem0  14813  nconstwlpolem  14815