Theorem ecased 1308

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 302	. 2 |- ( ph -> ( -. ch /\ ( ps \/ ch ) ) )
4		orel2 698	. . 3 |- ( -. ch -> ( ( ps \/ ch ) -> ps ) )
5	4	imp 123	. 2 |- ( ( -. ch /\ ( ps \/ ch ) ) -> ps )
6	3, 5	syl 14	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ wo 680

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 587  ax-io 681

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ecase23d  1309  preleq  4428  ordsuc  4436  reg3exmidlemwe  4451  sotri3  4893  diffisn  6738  onunsnss  6756  fival  6808  suplub2ti  6838  fodjum  6966  addnqprlemfl  7309  addnqprlemfu  7310  mulnqprlemfl  7325  mulnqprlemfu  7326  addcanprleml  7364  addcanprlemu  7365  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  caucvgprlemladdrl  7428  caucvgprprlemaddq  7458  ltletr  7770  apreap  8261  ltleap  8305  uzm1  9252  xrltletr  9477  xaddf  9514  xaddval  9515  iseqf1olemqcl  10146  iseqf1olemnab  10148  iseqf1olemab  10149  exp3val  10182  zfz1isolemiso  10469  ltabs  10745  xrmaxiflemlub  10903  bezoutlemmain  11526  nninfalllem1  12884  nninfall  12885  nninfsellemqall  12892  nninffeq  12897  trilpolemeq1  12914