Theorem orcd 723

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

Syntax hints:   -> wi 4   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  724  pm2.47  730  orim12i  749  animorl  813  animorrl  816  dcor  925  undif3ss  3382  dcun  3518  exmidn0m  4179  exmidsssn  4180  reg2exmidlema  4510  acexmidlem1  5837  poxp  6196  nntri2or2  6462  nnm00  6493  ssfilem  6837  diffitest  6849  tridc  6861  finexdc  6864  fientri3  6876  unsnfidcex  6881  unsnfidcel  6882  fidcenumlemrks  6914  nninfisollem0  7090  nninfisollemeq  7092  finomni  7100  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  exmidontriimlem2  7174  nqprloc  7482  mullocprlem  7507  recexprlemloc  7568  ltxrlt  7960  zmulcl  9240  nn0lt2  9268  zeo  9292  xrltso  9728  xnn0dcle  9734  xnn0letri  9735  apbtwnz  10205  expnegap0  10459  xrmaxadd  11198  zsumdc  11321  fsumsplit  11344  sumsplitdc  11369  isumlessdc  11433  zproddc  11516  fprodsplitdc  11533  fprodsplit  11534  fprodunsn  11541  fprodcl2lem  11542  prm23ge5  12192  suplociccreex  13202  lgsdir2lem5  13533  djulclALT  13642  trilpolemres  13881  trirec0  13883  nconstwlpolem0  13901  nconstwlpolem  13903