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  3319  ssdifin0  3631  uneqdifeq  3638  unimax  3925  pw1exg  4302  cokexg  4309  pwexg  4328  nnsucelr  4428  vfinspnn  4541  isoini2  5498  fullfunexg  5859  qsexg  5982  mapsn  6026  enrflxg  6034  cnven  6045  ncdisjun  6136  addccan2nclem2  6264  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  nchoicelem1  6289  nchoicelem2  6290  nchoicelem12  6300  frec0  6321