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  8917  ltleap  8962  uzm1  9962  xrltletr  10219  xaddf  10256  xaddval  10257  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemab  10952  exp3val  10991  zfz1isolemiso  11305  ltabs  11868  xrmaxiflemlub  12030  fprodsplitdc  12379  fprodcl2lem  12388  bitsfzo  12738  bezoutlemmain  12791  nninfctlemfo  12833  4sqlem17  13206  4sqlem18  13207  plycoeid3  15907  dvply1  15915  ppinprm  16171  perfectlem2  16198  lgsval  16221  lgsfvalg  16222  lgsdilem  16244  lgsdir  16252  lgsabs1  16256  gausslemma2dlem1f1o  16277  lgseisenlem1  16287  2sqlem7  16338  clwwlknnn  16751  nninfalllem1  17149  nninfall  17150  nninfsellemqall  17156  nninffeq  17161  nninfnfiinf  17164  trilpolemeq1  17187  nconstwlpolem  17213