Theorem orcd 745

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

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  olcd  746  pm2.47  752  orim12i  771  animorl  835  animorrl  838  dcor  948  dfifp2dc  994  undif3ss  3492  dcun  3637  ifeqeqxdc  3687  rabsnifsb  3777  exmidn0m  4340  exmidsssn  4341  reg2exmidlema  4683  acexmidlem1  6084  poxp  6472  nntri2or2  6776  nnm00  6808  ssfilem  7183  ssfilemd  7185  diffitest  7197  tridc  7210  finexdc  7213  elssdc  7215  fientri3  7228  unsnfidcex  7233  unsnfidcel  7234  fidcenumlemrks  7277  fdcf1  7321  nninfisollem0  7476  nninfisollemeq  7478  finomni  7486  pr1or2  7546  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  exmidontriimlem2  7584  netap  7626  2omotaplemap  7629  nqprloc  7918  mullocprlem  7943  recexprlemloc  8004  ltxrlt  8397  zmulcl  9707  nn0lt2  9736  zeo  9761  xrltso  10214  xnn0dcle  10220  xnn0letri  10221  apbtwnz  10725  expnegap0  11004  resq01  11115  fzowrddc  11440  xrmaxadd  12051  zsumdc  12175  fsumsplit  12198  sumsplitdc  12223  isumlessdc  12287  zproddc  12370  fprodsplitdc  12387  fprodsplit  12388  fprodunsn  12395  fprodcl2lem  12396  prm23ge5  13071  pcxqcl  13119  gzsum0  13771  lringuplu  14611  aprlring  14708  suplociccreex  15867  lgsdir2lem5  16373  usgredg2v  16687  dichmul0orlem3  16977  dichmul0orlem7  16981  djulclALT  17051  trilpolemres  17315  trirec0  17317  nconstwlpolem0  17337  nconstwlpolem  17339