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  3758  ontriexmidim  4644  preleq  4677  ordsuc  4685  reg3exmidlemwe  4701  sotri3  5161  pw2f1odclem  7087  diffisn  7150  onunsnss  7177  fival  7257  2omap  7269  suplub2ti  7292  fodjum  7437  nninfwlpoimlemginf  7467  3nelsucpw1  7544  3nsssucpw1  7546  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemfl  7890  mulnqprlemfu  7891  addcanprleml  7929  addcanprlemu  7930  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  caucvgprprlemaddq  8023  ltletr  8363  apreap  8861  ltleap  8906  uzm1  9885  xrltletr  10140  xaddf  10177  xaddval  10178  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemab  10864  exp3val  10903  zfz1isolemiso  11211  ltabs  11772  xrmaxiflemlub  11933  fprodsplitdc  12282  fprodcl2lem  12291  bitsfzo  12641  bezoutlemmain  12694  nninfctlemfo  12736  4sqlem17  13105  4sqlem18  13106  plycoeid3  15622  dvply1  15630  perfectlem2  15868  lgsval  15877  lgsfvalg  15878  lgsdilem  15900  lgsdir  15908  lgsabs1  15912  gausslemma2dlem1f1o  15933  lgseisenlem1  15943  2sqlem7  15994  clwwlknnn  16407  nninfalllem1  16786  nninfall  16787  nninfsellemqall  16793  nninffeq  16798  nninfnfiinf  16801  trilpolemeq1  16824  nconstwlpolem  16851