Theorem ecased 1386

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 734	. . 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 716

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 620  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1387  ecase2d  1388  rabsnif  3742  ontriexmidim  4626  preleq  4659  ordsuc  4667  reg3exmidlemwe  4683  sotri3  5142  pw2f1odclem  7063  diffisn  7125  onunsnss  7152  fival  7212  suplub2ti  7243  fodjum  7388  nninfwlpoimlemginf  7418  3nelsucpw1  7495  3nsssucpw1  7497  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemfl  7838  mulnqprlemfu  7839  addcanprleml  7877  addcanprlemu  7878  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  caucvgprprlemaddq  7971  ltletr  8311  apreap  8809  ltleap  8854  uzm1  9831  xrltletr  10086  xaddf  10123  xaddval  10124  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemab  10810  exp3val  10849  zfz1isolemiso  11149  ltabs  11710  xrmaxiflemlub  11871  fprodsplitdc  12220  fprodcl2lem  12229  bitsfzo  12579  bezoutlemmain  12632  nninfctlemfo  12674  4sqlem17  13043  4sqlem18  13044  plycoeid3  15551  dvply1  15559  perfectlem2  15797  lgsval  15806  lgsfvalg  15807  lgsdilem  15829  lgsdir  15837  lgsabs1  15841  gausslemma2dlem1f1o  15862  lgseisenlem1  15872  2sqlem7  15923  clwwlknnn  16336  2omap  16698  nninfalllem1  16717  nninfall  16718  nninfsellemqall  16724  nninffeq  16729  nninfnfiinf  16732  trilpolemeq1  16755  nconstwlpolem  16781