Theorem sylanl1 402

Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.)

Hypotheses

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

Assertion

Ref	Expression
sylanl1	|- ( ( ( ph /\ ch ) /\ th ) -> ta )

Proof of Theorem sylanl1

Step	Hyp	Ref	Expression
1		sylanl1.1	. . 3 |- ( ph -> ps )
2	1	anim1i 340	. 2 |- ( ( ph /\ ch ) -> ( ps /\ ch ) )
3		sylanl1.2	. 2 |- ( ( ( ps /\ ch ) /\ th ) -> ta )
4	2, 3	sylan 283	1 |- ( ( ( ph /\ ch ) /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  adantlll  480  adantllr  481  adantl3r  512  isocnv  5947  mapxpen  7029  nqnq0pi  7648  nqpnq0nq  7663  addnqprl  7739  addnqpru  7740  pcqmul  12866  infpnlem1  12922  setsn0fun  13109  gsumfzz  13568  dvmptfsum  15439  usgr2edg  16047  usgr2edg1  16049