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  3763  ontriexmidim  4649  preleq  4682  ordsuc  4690  reg3exmidlemwe  4706  sotri3  5166  pw2f1odclem  7100  diffisn  7163  onunsnss  7190  fival  7270  2omap  7282  suplub2ti  7305  fodjum  7450  nninfwlpoimlemginf  7480  3nelsucpw1  7557  3nsssucpw1  7559  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemfl  7906  mulnqprlemfu  7907  addcanprleml  7945  addcanprlemu  7946  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgprprlemaddq  8039  ltletr  8379  apreap  8878  ltleap  8923  uzm1  9903  xrltletr  10159  xaddf  10196  xaddval  10197  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  exp3val  10927  zfz1isolemiso  11236  ltabs  11797  xrmaxiflemlub  11958  fprodsplitdc  12307  fprodcl2lem  12316  bitsfzo  12666  bezoutlemmain  12719  nninfctlemfo  12761  4sqlem17  13130  4sqlem18  13131  plycoeid3  15748  dvply1  15756  perfectlem2  15994  lgsval  16003  lgsfvalg  16004  lgsdilem  16026  lgsdir  16034  lgsabs1  16038  gausslemma2dlem1f1o  16059  lgseisenlem1  16069  2sqlem7  16120  clwwlknnn  16533  nninfalllem1  16912  nninfall  16913  nninfsellemqall  16919  nninffeq  16924  nninfnfiinf  16927  trilpolemeq1  16950  nconstwlpolem  16977