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  7319  suplub2ti  7342  fodjum  7487  nninfwlpoimlemginf  7517  3nelsucpw1  7594  3nsssucpw1  7596  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemfl  7943  mulnqprlemfu  7944  addcanprleml  7982  addcanprlemu  7983  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  caucvgprprlemaddq  8076  ltletr  8416  apreap  8918  ltleap  8963  uzm1  9963  xrltletr  10220  xaddf  10257  xaddval  10258  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemab  10954  exp3val  10993  zfz1isolemiso  11307  ltabs  11870  xrmaxiflemlub  12033  fprodsplitdc  12382  fprodcl2lem  12391  bitsfzo  12741  bezoutlemmain  12794  nninfctlemfo  12836  4sqlem17  13209  4sqlem18  13210  plycoeid3  15949  dvply1  15957  ppinprm  16221  chtnprm  16223  perfectlem2  16261  lgsval  16289  lgsfvalg  16290  lgsdilem  16312  lgsdir  16320  lgsabs1  16324  gausslemma2dlem1f1o  16345  lgseisenlem1  16355  2sqlem7  16406  clwwlknnn  16819  nninfalllem1  17217  nninfall  17218  nninfsellemqall  17224  nninffeq  17229  nninfnfiinf  17232  trilpolemeq1  17256  nconstwlpolem  17282