Theorem biimtrrid

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

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

Proof

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