Theorem ecased 1362

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 728	. . 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 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1363  ontriexmidim  4570  preleq  4603  ordsuc  4611  reg3exmidlemwe  4627  sotri3  5081  pw2f1odclem  6931  diffisn  6990  onunsnss  7014  fival  7072  suplub2ti  7103  fodjum  7248  nninfwlpoimlemginf  7278  3nelsucpw1  7346  3nsssucpw1  7348  addnqprlemfl  7672  addnqprlemfu  7673  mulnqprlemfl  7688  mulnqprlemfu  7689  addcanprleml  7727  addcanprlemu  7728  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemladdrl  7791  caucvgprprlemaddq  7821  ltletr  8162  apreap  8660  ltleap  8705  uzm1  9679  xrltletr  9929  xaddf  9966  xaddval  9967  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  exp3val  10686  zfz1isolemiso  10984  ltabs  11398  xrmaxiflemlub  11559  fprodsplitdc  11907  fprodcl2lem  11916  bitsfzo  12266  bezoutlemmain  12319  nninfctlemfo  12361  4sqlem17  12730  4sqlem18  12731  plycoeid3  15229  dvply1  15237  perfectlem2  15472  lgsval  15481  lgsfvalg  15482  lgsdilem  15504  lgsdir  15512  lgsabs1  15516  gausslemma2dlem1f1o  15537  lgseisenlem1  15547  2sqlem7  15598  2omap  15932  nninfalllem1  15945  nninfall  15946  nninfsellemqall  15952  nninffeq  15957  nninfnfiinf  15960  trilpolemeq1  15979  nconstwlpolem  16004