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  6775  nnm00  6807  ssfilem  7181  ssfilemd  7183  diffitest  7195  tridc  7208  finexdc  7211  elssdc  7213  fientri3  7226  unsnfidcex  7231  unsnfidcel  7232  fidcenumlemrks  7275  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  9709  nn0lt2  9738  zeo  9762  xrltso  10215  xnn0dcle  10221  xnn0letri  10222  apbtwnz  10726  expnegap0  11005  resq01  11116  fzowrddc  11441  xrmaxadd  12052  zsumdc  12176  fsumsplit  12199  sumsplitdc  12224  isumlessdc  12288  zproddc  12371  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodcl2lem  12397  prm23ge5  13072  pcxqcl  13120  gzsum0  13772  lringuplu  14612  aprlring  14709  suplociccreex  15850  lgsdir2lem5  16356  usgredg2v  16670  dichmul0orlem3  16960  dichmul0orlem7  16964  djulclALT  17034  trilpolemres  17298  trirec0  17300  nconstwlpolem0  17320  nconstwlpolem  17322