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  5990  mapxpen  7114  nqnq0pi  7769  nqpnq0nq  7784  addnqprl  7860  addnqpru  7861  pcqmul  13026  infpnlem1  13082  setsn0fun  13333  gsumfzz  13750  dvmptfsum  15716  usgr2edg  16329  usgr2edg1  16331