Theorem ecased 1339

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  1340  ontriexmidim  4499  preleq  4532  ordsuc  4540  reg3exmidlemwe  4556  sotri3  5002  diffisn  6859  onunsnss  6882  fival  6935  suplub2ti  6966  fodjum  7110  3nelsucpw1  7190  3nsssucpw1  7192  addnqprlemfl  7500  addnqprlemfu  7501  mulnqprlemfl  7516  mulnqprlemfu  7517  addcanprleml  7555  addcanprlemu  7556  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgprlemladdrl  7619  caucvgprprlemaddq  7649  ltletr  7988  apreap  8485  ltleap  8530  uzm1  9496  xrltletr  9743  xaddf  9780  xaddval  9781  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemab  10424  exp3val  10457  zfz1isolemiso  10752  ltabs  11029  xrmaxiflemlub  11189  fprodsplitdc  11537  fprodcl2lem  11546  bezoutlemmain  11931  lgsval  13545  lgsfvalg  13546  lgsdilem  13568  lgsdir  13576  lgsabs1  13580  2sqlem7  13597  nninfalllem1  13888  nninfall  13889  nninfsellemqall  13895  nninffeq  13900  trilpolemeq1  13919  nconstwlpolem  13943