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  4614  preleq  4647  ordsuc  4655  reg3exmidlemwe  4671  sotri3  5127  pw2f1odclem  6995  diffisn  7055  onunsnss  7079  fival  7137  suplub2ti  7168  fodjum  7313  nninfwlpoimlemginf  7343  3nelsucpw1  7419  3nsssucpw1  7421  addnqprlemfl  7746  addnqprlemfu  7747  mulnqprlemfl  7762  mulnqprlemfu  7763  addcanprleml  7801  addcanprlemu  7802  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgprlemladdrl  7865  caucvgprprlemaddq  7895  ltletr  8236  apreap  8734  ltleap  8779  uzm1  9753  xrltletr  10003  xaddf  10040  xaddval  10041  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemab  10724  exp3val  10763  zfz1isolemiso  11061  ltabs  11598  xrmaxiflemlub  11759  fprodsplitdc  12107  fprodcl2lem  12116  bitsfzo  12466  bezoutlemmain  12519  nninfctlemfo  12561  4sqlem17  12930  4sqlem18  12931  plycoeid3  15431  dvply1  15439  perfectlem2  15674  lgsval  15683  lgsfvalg  15684  lgsdilem  15706  lgsdir  15714  lgsabs1  15718  gausslemma2dlem1f1o  15739  lgseisenlem1  15749  2sqlem7  15800  2omap  16359  nninfalllem1  16374  nninfall  16375  nninfsellemqall  16381  nninffeq  16386  nninfnfiinf  16389  trilpolemeq1  16408  nconstwlpolem  16433