Theorem sylancb

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

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

Proof

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