Theorem syl5bir

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypotheses	syl5bir.1	|- ( ps <-> ph )
	syl5bir.2	|- ( ch -> ( ps -> th ) )
Assertion	syl5bir	|- ( ch -> ( ph -> th ) )

Proof

Step	Hyp	Ref	Expression
1		syl5bir.1	|- ( ps <-> ph )
2		syl5bir.2	|- ( ch -> ( ps -> th ) )
3	1	biimpri	|- ( ph -> ps )
4	3 2	syl5	|- ( ch -> ( ph -> th ) )