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  7003  diffisn  7063  onunsnss  7090  fival  7148  suplub2ti  7179  fodjum  7324  nninfwlpoimlemginf  7354  3nelsucpw1  7430  3nsssucpw1  7432  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemfl  7773  mulnqprlemfu  7774  addcanprleml  7812  addcanprlemu  7813  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  caucvgprprlemaddq  7906  ltletr  8247  apreap  8745  ltleap  8790  uzm1  9765  xrltletr  10015  xaddf  10052  xaddval  10053  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  exp3val  10775  zfz1isolemiso  11074  ltabs  11613  xrmaxiflemlub  11774  fprodsplitdc  12122  fprodcl2lem  12131  bitsfzo  12481  bezoutlemmain  12534  nninfctlemfo  12576  4sqlem17  12945  4sqlem18  12946  plycoeid3  15446  dvply1  15454  perfectlem2  15689  lgsval  15698  lgsfvalg  15699  lgsdilem  15721  lgsdir  15729  lgsabs1  15733  gausslemma2dlem1f1o  15754  lgseisenlem1  15764  2sqlem7  15815  2omap  16418  nninfalllem1  16434  nninfall  16435  nninfsellemqall  16441  nninffeq  16446  nninfnfiinf  16449  trilpolemeq1  16468  nconstwlpolem  16493