Theorem syl2anbr

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

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

Proof

Step	Hyp	Ref	Expression
1		syl2anbr.1	|- ( ps <-> ph )
2		syl2anbr.2	|- ( ch <-> ta )
3		syl2anbr.3	|- ( ( ps /\ ch ) -> th )
4	1 3	sylanbr	|- ( ( ph /\ ch ) -> th )
5	2 4	sylan2br	|- ( ( ph /\ ta ) -> th )