Theorem ecased 1360

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 727	. . 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 709

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 616  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1361  ontriexmidim  4554  preleq  4587  ordsuc  4595  reg3exmidlemwe  4611  sotri3  5064  pw2f1odclem  6890  diffisn  6949  onunsnss  6973  fival  7029  suplub2ti  7060  fodjum  7205  nninfwlpoimlemginf  7235  3nelsucpw1  7294  3nsssucpw1  7296  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemfl  7635  mulnqprlemfu  7636  addcanprleml  7674  addcanprlemu  7675  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  caucvgprprlemaddq  7768  ltletr  8109  apreap  8606  ltleap  8651  uzm1  9623  xrltletr  9873  xaddf  9910  xaddval  9911  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  exp3val  10612  zfz1isolemiso  10910  ltabs  11231  xrmaxiflemlub  11391  fprodsplitdc  11739  fprodcl2lem  11748  bezoutlemmain  12135  nninfctlemfo  12177  4sqlem17  12545  4sqlem18  12546  lgsval  15120  lgsfvalg  15121  lgsdilem  15143  lgsdir  15151  lgsabs1  15155  gausslemma2dlem1f1o  15176  lgseisenlem1  15186  2sqlem7  15208  nninfalllem1  15498  nninfall  15499  nninfsellemqall  15505  nninffeq  15510  trilpolemeq1  15530  nconstwlpolem  15555