Theorem ecased 1349

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 726	. . 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 708

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 615  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1350  ontriexmidim  4522  preleq  4555  ordsuc  4563  reg3exmidlemwe  4579  sotri3  5028  diffisn  6893  onunsnss  6916  fival  6969  suplub2ti  7000  fodjum  7144  nninfwlpoimlemginf  7174  3nelsucpw1  7233  3nsssucpw1  7235  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemfl  7574  mulnqprlemfu  7575  addcanprleml  7613  addcanprlemu  7614  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemladdrl  7677  caucvgprprlemaddq  7707  ltletr  8047  apreap  8544  ltleap  8589  uzm1  9558  xrltletr  9807  xaddf  9844  xaddval  9845  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemab  10489  exp3val  10522  zfz1isolemiso  10819  ltabs  11096  xrmaxiflemlub  11256  fprodsplitdc  11604  fprodcl2lem  11613  bezoutlemmain  11999  lgsval  14408  lgsfvalg  14409  lgsdilem  14431  lgsdir  14439  lgsabs1  14443  lgseisenlem1  14453  2sqlem7  14471  nninfalllem1  14760  nninfall  14761  nninfsellemqall  14767  nninffeq  14772  trilpolemeq1  14791  nconstwlpolem  14815