Theorem syl2anb

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999)

	Ref	Expression
Hypotheses	syl2anb.1	|- ( ph <-> ps )
	syl2anb.2	|- ( ta <-> ch )
	syl2anb.3	|- ( ( ps /\ ch ) -> th )
Assertion	syl2anb	|- ( ( ph /\ ta ) -> th )

Proof

Step	Hyp	Ref	Expression
1		syl2anb.1	|- ( ph <-> ps )
2		syl2anb.2	|- ( ta <-> ch )
3		syl2anb.3	|- ( ( ps /\ ch ) -> th )
4	1 3	sylanb	|- ( ( ph /\ ch ) -> th )
5	2 4	sylan2b	|- ( ( ph /\ ta ) -> th )