Theorem ecased 1390

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 738	. . 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 720

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 624  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1391  ecase2d  1392  rabsnif  3774  ontriexmidim  4664  preleq  4697  ordsuc  4705  reg3exmidlemwe  4721  sotri3  5181  pw2f1odclem  7124  diffisn  7187  onunsnss  7214  fival  7294  2omap  7308  suplub2ti  7331  fodjum  7476  nninfwlpoimlemginf  7506  3nelsucpw1  7583  3nsssucpw1  7585  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemfl  7932  mulnqprlemfu  7933  addcanprleml  7971  addcanprlemu  7972  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  caucvgprprlemaddq  8065  ltletr  8405  apreap  8905  ltleap  8950  uzm1  9932  xrltletr  10188  xaddf  10225  xaddval  10226  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemab  10917  exp3val  10956  zfz1isolemiso  11269  ltabs  11831  xrmaxiflemlub  11992  fprodsplitdc  12341  fprodcl2lem  12350  bitsfzo  12700  bezoutlemmain  12753  nninfctlemfo  12795  4sqlem17  13164  4sqlem18  13165  plycoeid3  15781  dvply1  15789  perfectlem2  16028  lgsval  16037  lgsfvalg  16038  lgsdilem  16060  lgsdir  16068  lgsabs1  16072  gausslemma2dlem1f1o  16093  lgseisenlem1  16103  2sqlem7  16154  clwwlknnn  16567  nninfalllem1  16956  nninfall  16957  nninfsellemqall  16963  nninffeq  16968  nninfnfiinf  16971  trilpolemeq1  16994  nconstwlpolem  17020