Theorem ecased 1362

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 728	. . 3 |- ( -. ch -> ( ( ps \/ ch ) -> ps ) )
5	4	imp 124	. 2 |- ( ( -. ch /\ ( ps \/ ch ) ) -> ps )
6	3, 5	syl 14	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1363  ontriexmidim  4588  preleq  4621  ordsuc  4629  reg3exmidlemwe  4645  sotri3  5100  pw2f1odclem  6956  diffisn  7016  onunsnss  7040  fival  7098  suplub2ti  7129  fodjum  7274  nninfwlpoimlemginf  7304  3nelsucpw1  7380  3nsssucpw1  7382  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprlemfl  7723  mulnqprlemfu  7724  addcanprleml  7762  addcanprlemu  7763  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemladdrl  7826  caucvgprprlemaddq  7856  ltletr  8197  apreap  8695  ltleap  8740  uzm1  9714  xrltletr  9964  xaddf  10001  xaddval  10002  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  exp3val  10723  zfz1isolemiso  11021  ltabs  11513  xrmaxiflemlub  11674  fprodsplitdc  12022  fprodcl2lem  12031  bitsfzo  12381  bezoutlemmain  12434  nninfctlemfo  12476  4sqlem17  12845  4sqlem18  12846  plycoeid3  15344  dvply1  15352  perfectlem2  15587  lgsval  15596  lgsfvalg  15597  lgsdilem  15619  lgsdir  15627  lgsabs1  15631  gausslemma2dlem1f1o  15652  lgseisenlem1  15662  2sqlem7  15713  2omap  16132  nninfalllem1  16147  nninfall  16148  nninfsellemqall  16154  nninffeq  16159  nninfnfiinf  16162  trilpolemeq1  16181  nconstwlpolem  16206