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  5962  mapxpen  7077  nqnq0pi  7701  nqpnq0nq  7716  addnqprl  7792  addnqpru  7793  pcqmul  12939  infpnlem1  12995  setsn0fun  13182  gsumfzz  13641  dvmptfsum  15519  usgr2edg  16132  usgr2edg1  16134