Theorem ecased 1349

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 726	. . 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 708

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 615  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1350  ontriexmidim  4521  preleq  4554  ordsuc  4562  reg3exmidlemwe  4578  sotri3  5027  diffisn  6892  onunsnss  6915  fival  6968  suplub2ti  6999  fodjum  7143  nninfwlpoimlemginf  7173  3nelsucpw1  7232  3nsssucpw1  7234  addnqprlemfl  7557  addnqprlemfu  7558  mulnqprlemfl  7573  mulnqprlemfu  7574  addcanprleml  7612  addcanprlemu  7613  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  caucvgprlemladdrl  7676  caucvgprprlemaddq  7706  ltletr  8046  apreap  8543  ltleap  8588  uzm1  9557  xrltletr  9806  xaddf  9843  xaddval  9844  iseqf1olemqcl  10485  iseqf1olemnab  10487  iseqf1olemab  10488  exp3val  10521  zfz1isolemiso  10818  ltabs  11095  xrmaxiflemlub  11255  fprodsplitdc  11603  fprodcl2lem  11612  bezoutlemmain  11998  lgsval  14375  lgsfvalg  14376  lgsdilem  14398  lgsdir  14406  lgsabs1  14410  lgseisenlem1  14420  2sqlem7  14438  nninfalllem1  14727  nninfall  14728  nninfsellemqall  14734  nninffeq  14739  trilpolemeq1  14758  nconstwlpolem  14782