Theorem sylancl 643

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancl.1	|- (ph -> ps)
sylancl.2	|- ch
sylancl.3	|- ((ps /\ ch) -> th)

Assertion

Ref	Expression
sylancl	|- (ph -> th)

Proof of Theorem sylancl

Step	Hyp	Ref	Expression
1		sylancl.1	. 2 |- (ph -> ps)
2		sylancl.2	. . 3 |- ch
3	2	a1i 10	. 2 |- (ph -> ch)
4		sylancl.3	. 2 |- ((ps /\ ch) -> th)
5	1, 3, 4	syl2anc 642	1 |- (ph -> th)

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  equveli  1988  syl5sseq  3320  ssdifin0  3632  uneqdifeq  3639  unimax  3926  pw1exg  4303  cokexg  4310  pwexg  4329  nnsucelr  4429  vfinspnn  4542  isoini2  5499  fullfunexg  5860  qsexg  5983  mapsn  6027  enrflxg  6035  cnven  6046  ncdisjun  6137  addccan2nclem2  6265  nncdiv3  6278  nnc3n3p1  6279  nnc3n3p2  6280  nchoicelem1  6290  nchoicelem2  6291  nchoicelem12  6301  frec0  6322