Theorem ecased 1361

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  1362  ontriexmidim  4569  preleq  4602  ordsuc  4610  reg3exmidlemwe  4626  sotri3  5080  pw2f1odclem  6930  diffisn  6989  onunsnss  7013  fival  7071  suplub2ti  7102  fodjum  7247  nninfwlpoimlemginf  7277  3nelsucpw1  7345  3nsssucpw1  7347  addnqprlemfl  7671  addnqprlemfu  7672  mulnqprlemfl  7687  mulnqprlemfu  7688  addcanprleml  7726  addcanprlemu  7727  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemladdrl  7790  caucvgprprlemaddq  7820  ltletr  8161  apreap  8659  ltleap  8704  uzm1  9678  xrltletr  9928  xaddf  9965  xaddval  9966  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemab  10645  exp3val  10684  zfz1isolemiso  10982  ltabs  11369  xrmaxiflemlub  11530  fprodsplitdc  11878  fprodcl2lem  11887  bitsfzo  12237  bezoutlemmain  12290  nninfctlemfo  12332  4sqlem17  12701  4sqlem18  12702  plycoeid3  15200  dvply1  15208  perfectlem2  15443  lgsval  15452  lgsfvalg  15453  lgsdilem  15475  lgsdir  15483  lgsabs1  15487  gausslemma2dlem1f1o  15508  lgseisenlem1  15518  2sqlem7  15569  2omap  15894  nninfalllem1  15907  nninfall  15908  nninfsellemqall  15914  nninffeq  15919  nninfnfiinf  15922  trilpolemeq1  15941  nconstwlpolem  15966