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  7140  diffisn  7203  onunsnss  7230  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  9968  xrltletr  10225  xaddf  10262  xaddval  10263  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemab  10959  exp3val  10998  zfz1isolemiso  11312  ltabs  11875  xrmaxiflemlub  12038  fprodsplitdc  12387  fprodcl2lem  12396  bitsfzo  12746  bezoutlemmain  12799  nninfctlemfo  12841  4sqlem17  13214  4sqlem18  13215  plycoeid3  16000  dvply1  16008  ppinprm  16277  chtnprm  16279  perfectlem2  16317  lgsval  16345  lgsfvalg  16346  lgsdilem  16368  lgsdir  16376  lgsabs1  16380  gausslemma2dlem1f1o  16401  lgseisenlem1  16411  2sqlem7  16462  clwwlknnn  16875  idjudju  17269  nninfalllem1  17274  nninfall  17275  nninfsellemqall  17281  nninffeq  17286  nninfnfiinf  17289  trilpolemeq1  17313  nconstwlpolem  17339