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  rabsnif  3736  ontriexmidim  4618  preleq  4651  ordsuc  4659  reg3exmidlemwe  4675  sotri3  5133  pw2f1odclem  7015  diffisn  7075  onunsnss  7102  fival  7160  suplub2ti  7191  fodjum  7336  nninfwlpoimlemginf  7366  3nelsucpw1  7442  3nsssucpw1  7444  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemfl  7785  mulnqprlemfu  7786  addcanprleml  7824  addcanprlemu  7825  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  caucvgprprlemaddq  7918  ltletr  8259  apreap  8757  ltleap  8802  uzm1  9777  xrltletr  10032  xaddf  10069  xaddval  10070  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  exp3val  10793  zfz1isolemiso  11093  ltabs  11638  xrmaxiflemlub  11799  fprodsplitdc  12147  fprodcl2lem  12156  bitsfzo  12506  bezoutlemmain  12559  nninfctlemfo  12601  4sqlem17  12970  4sqlem18  12971  plycoeid3  15471  dvply1  15479  perfectlem2  15714  lgsval  15723  lgsfvalg  15724  lgsdilem  15746  lgsdir  15754  lgsabs1  15758  gausslemma2dlem1f1o  15779  lgseisenlem1  15789  2sqlem7  15840  clwwlknnn  16207  2omap  16530  nninfalllem1  16546  nninfall  16547  nninfsellemqall  16553  nninffeq  16558  nninfnfiinf  16561  trilpolemeq1  16580  nconstwlpolem  16605