Theorem ecased 1383

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 731	. . 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 713

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 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1384  ecase2d  1385  ontriexmidim  4613  preleq  4646  ordsuc  4654  reg3exmidlemwe  4670  sotri3  5126  pw2f1odclem  6991  diffisn  7051  onunsnss  7075  fival  7133  suplub2ti  7164  fodjum  7309  nninfwlpoimlemginf  7339  3nelsucpw1  7415  3nsssucpw1  7417  addnqprlemfl  7742  addnqprlemfu  7743  mulnqprlemfl  7758  mulnqprlemfu  7759  addcanprleml  7797  addcanprlemu  7798  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  caucvgprprlemaddq  7891  ltletr  8232  apreap  8730  ltleap  8775  uzm1  9749  xrltletr  9999  xaddf  10036  xaddval  10037  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemab  10719  exp3val  10758  zfz1isolemiso  11056  ltabs  11593  xrmaxiflemlub  11754  fprodsplitdc  12102  fprodcl2lem  12111  bitsfzo  12461  bezoutlemmain  12514  nninfctlemfo  12556  4sqlem17  12925  4sqlem18  12926  plycoeid3  15425  dvply1  15433  perfectlem2  15668  lgsval  15677  lgsfvalg  15678  lgsdilem  15700  lgsdir  15708  lgsabs1  15712  gausslemma2dlem1f1o  15733  lgseisenlem1  15743  2sqlem7  15794  2omap  16318  nninfalllem1  16333  nninfall  16334  nninfsellemqall  16340  nninffeq  16345  nninfnfiinf  16348  trilpolemeq1  16367  nconstwlpolem  16392