Theorem ecased 1344

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 721	. . 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 703

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 610  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ecase23d  1345  ontriexmidim  4506  preleq  4539  ordsuc  4547  reg3exmidlemwe  4563  sotri3  5009  diffisn  6871  onunsnss  6894  fival  6947  suplub2ti  6978  fodjum  7122  nninfwlpoimlemginf  7152  3nelsucpw1  7211  3nsssucpw1  7213  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemfl  7537  mulnqprlemfu  7538  addcanprleml  7576  addcanprlemu  7577  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  caucvgprprlemaddq  7670  ltletr  8009  apreap  8506  ltleap  8551  uzm1  9517  xrltletr  9764  xaddf  9801  xaddval  9802  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemab  10445  exp3val  10478  zfz1isolemiso  10774  ltabs  11051  xrmaxiflemlub  11211  fprodsplitdc  11559  fprodcl2lem  11568  bezoutlemmain  11953  lgsval  13699  lgsfvalg  13700  lgsdilem  13722  lgsdir  13730  lgsabs1  13734  2sqlem7  13751  nninfalllem1  14041  nninfall  14042  nninfsellemqall  14048  nninffeq  14053  trilpolemeq1  14072  nconstwlpolem  14096