Theorem ecased 1328

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ecase23d  1329  ontriexmidim  4475  preleq  4508  ordsuc  4516  reg3exmidlemwe  4532  sotri3  4977  diffisn  6827  onunsnss  6850  fival  6903  suplub2ti  6933  fodjum  7068  3nelsucpw1  7148  3nsssucpw1  7150  addnqprlemfl  7458  addnqprlemfu  7459  mulnqprlemfl  7474  mulnqprlemfu  7475  addcanprleml  7513  addcanprlemu  7514  cauappcvgprlemladdru  7555  cauappcvgprlemladdrl  7556  caucvgprlemladdrl  7577  caucvgprprlemaddq  7607  ltletr  7945  apreap  8441  ltleap  8486  uzm1  9448  xrltletr  9689  xaddf  9726  xaddval  9727  iseqf1olemqcl  10363  iseqf1olemnab  10365  iseqf1olemab  10366  exp3val  10399  zfz1isolemiso  10687  ltabs  10964  xrmaxiflemlub  11122  fprodsplitdc  11470  fprodcl2lem  11479  bezoutlemmain  11853  nninfalllem1  13521  nninfall  13522  nninfsellemqall  13528  nninffeq  13533  trilpolemeq1  13552  nconstwlpolem  13576