Theorem sylancbr

Description: A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004)

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

Proof

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