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  4671  preleq  4704  ordsuc  4712  reg3exmidlemwe  4728  sotri3  5189  pw2f1odclem  7138  diffisn  7201  onunsnss  7228  fival  7309  2omap  7324  suplub2ti  7347  fodjum  7492  nninfwlpoimlemginf  7522  3nelsucpw1  7599  3nsssucpw1  7601  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemfl  7948  mulnqprlemfu  7949  addcanprleml  7987  addcanprlemu  7988  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprprlemaddq  8081  ltletr  8421  apreap  8923  ltleap  8968  uzm1  9969  xrltletr  10226  xaddf  10263  xaddval  10264  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemab  10960  exp3val  10999  zfz1isolemiso  11313  ltabs  11876  xrmaxiflemlub  12039  fprodsplitdc  12388  fprodcl2lem  12397  bitsfzo  12747  bezoutlemmain  12800  nninfctlemfo  12842  4sqlem17  13215  4sqlem18  13216  plycoeid3  15983  dvply1  15991  ppinprm  16260  chtnprm  16262  perfectlem2  16300  lgsval  16328  lgsfvalg  16329  lgsdilem  16351  lgsdir  16359  lgsabs1  16363  gausslemma2dlem1f1o  16384  lgseisenlem1  16394  2sqlem7  16445  clwwlknnn  16858  idjudju  17252  nninfalllem1  17257  nninfall  17258  nninfsellemqall  17264  nninffeq  17269  nninfnfiinf  17272  trilpolemeq1  17296  nconstwlpolem  17322