Theorem ecased 1385

Description: Deduction form of disjunctive syllogism. (Contributed by Jim Kingdon, 9-Dec-2017.)

Hypotheses

Ref	Expression
ecased.1	|- ( ph -> -. ch )
ecased.2	|- ( ph -> ( ps \/ ch ) )

Assertion

Ref	Expression
ecased	|- ( ph -> ps )

Proof of Theorem ecased

Step	Hyp	Ref	Expression
1		ecased.1	. . 3 |- ( ph -> -. ch )
2		ecased.2	. . 3 |- ( ph -> ( ps \/ ch ) )
3	1, 2	jca 306	. 2 |- ( ph -> ( -. ch /\ ( ps \/ ch ) ) )
4		orel2 733	. . 3 |- ( -. ch -> ( ( ps \/ ch ) -> ps ) )
5	4	imp 124	. 2 |- ( ( -. ch /\ ( ps \/ ch ) ) -> ps )
6	3, 5	syl 14	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 620  ax-io 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1386  ecase2d  1387  rabsnif  3738  ontriexmidim  4620  preleq  4653  ordsuc  4661  reg3exmidlemwe  4677  sotri3  5135  pw2f1odclem  7019  diffisn  7081  onunsnss  7108  fival  7168  suplub2ti  7199  fodjum  7344  nninfwlpoimlemginf  7374  3nelsucpw1  7451  3nsssucpw1  7453  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemfl  7794  mulnqprlemfu  7795  addcanprleml  7833  addcanprlemu  7834  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  caucvgprprlemaddq  7927  ltletr  8268  apreap  8766  ltleap  8811  uzm1  9786  xrltletr  10041  xaddf  10078  xaddval  10079  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  exp3val  10802  zfz1isolemiso  11102  ltabs  11647  xrmaxiflemlub  11808  fprodsplitdc  12156  fprodcl2lem  12165  bitsfzo  12515  bezoutlemmain  12568  nninfctlemfo  12610  4sqlem17  12979  4sqlem18  12980  plycoeid3  15480  dvply1  15488  perfectlem2  15723  lgsval  15732  lgsfvalg  15733  lgsdilem  15755  lgsdir  15763  lgsabs1  15767  gausslemma2dlem1f1o  15788  lgseisenlem1  15798  2sqlem7  15849  clwwlknnn  16262  2omap  16594  nninfalllem1  16610  nninfall  16611  nninfsellemqall  16617  nninffeq  16622  nninfnfiinf  16625  trilpolemeq1  16644  nconstwlpolem  16669