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  7020  diffisn  7082  onunsnss  7109  fival  7169  suplub2ti  7200  fodjum  7345  nninfwlpoimlemginf  7375  3nelsucpw1  7452  3nsssucpw1  7454  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemfl  7795  mulnqprlemfu  7796  addcanprleml  7834  addcanprlemu  7835  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprprlemaddq  7928  ltletr  8269  apreap  8767  ltleap  8812  uzm1  9787  xrltletr  10042  xaddf  10079  xaddval  10080  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  exp3val  10804  zfz1isolemiso  11104  ltabs  11665  xrmaxiflemlub  11826  fprodsplitdc  12175  fprodcl2lem  12184  bitsfzo  12534  bezoutlemmain  12587  nninfctlemfo  12629  4sqlem17  12998  4sqlem18  12999  plycoeid3  15500  dvply1  15508  perfectlem2  15743  lgsval  15752  lgsfvalg  15753  lgsdilem  15775  lgsdir  15783  lgsabs1  15787  gausslemma2dlem1f1o  15808  lgseisenlem1  15818  2sqlem7  15869  clwwlknnn  16282  2omap  16645  nninfalllem1  16661  nninfall  16662  nninfsellemqall  16668  nninffeq  16673  nninfnfiinf  16676  trilpolemeq1  16695  nconstwlpolem  16721