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  4520  preleq  4553  ordsuc  4561  reg3exmidlemwe  4577  sotri3  5026  diffisn  6890  onunsnss  6913  fival  6966  suplub2ti  6997  fodjum  7141  nninfwlpoimlemginf  7171  3nelsucpw1  7230  3nsssucpw1  7232  addnqprlemfl  7555  addnqprlemfu  7556  mulnqprlemfl  7571  mulnqprlemfu  7572  addcanprleml  7610  addcanprlemu  7611  cauappcvgprlemladdru  7652  cauappcvgprlemladdrl  7653  caucvgprlemladdrl  7674  caucvgprprlemaddq  7704  ltletr  8043  apreap  8540  ltleap  8585  uzm1  9554  xrltletr  9803  xaddf  9840  xaddval  9841  iseqf1olemqcl  10481  iseqf1olemnab  10483  iseqf1olemab  10484  exp3val  10517  zfz1isolemiso  10812  ltabs  11089  xrmaxiflemlub  11249  fprodsplitdc  11597  fprodcl2lem  11606  bezoutlemmain  11991  lgsval  14276  lgsfvalg  14277  lgsdilem  14299  lgsdir  14307  lgsabs1  14311  2sqlem7  14328  nninfalllem1  14617  nninfall  14618  nninfsellemqall  14624  nninffeq  14629  trilpolemeq1  14648  nconstwlpolem  14672