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 )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 720

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used by:  ecase23d  1391  ecase2d  1392  rabsnif  3778  ontriexmidim  4669  preleq  4702  ordsuc  4710  reg3exmidlemwe  4726  sotri3  5186  pw2f1odclem  7134  diffisn  7197  onunsnss  7224  fival  7304  2omap  7318  suplub2ti  7341  fodjum  7486  nninfwlpoimlemginf  7516  3nelsucpw1  7593  3nsssucpw1  7595  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  addcanprleml  7981  addcanprlemu  7982  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  caucvgprprlemaddq  8075  ltletr  8415  apreap  8915  ltleap  8960  uzm1  9953  xrltletr  10209  xaddf  10246  xaddval  10247  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemab  10939  exp3val  10978  zfz1isolemiso  11291  ltabs  11853  xrmaxiflemlub  12014  fprodsplitdc  12363  fprodcl2lem  12372  bitsfzo  12722  bezoutlemmain  12775  nninfctlemfo  12817  4sqlem17  13186  4sqlem18  13187  plycoeid3  15858  dvply1  15866  perfectlem2  16114  lgsval  16123  lgsfvalg  16124  lgsdilem  16146  lgsdir  16154  lgsabs1  16158  gausslemma2dlem1f1o  16179  lgseisenlem1  16189  2sqlem7  16240  clwwlknnn  16653  nninfalllem1  17051  nninfall  17052  nninfsellemqall  17058  nninffeq  17063  nninfnfiinf  17066  trilpolemeq1  17089  nconstwlpolem  17115