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	⊢ ( 𝜓 ↔ 𝜑 )
	biimtrrid.2	⊢ ( 𝜒 → ( 𝜓 → 𝜃 ) )
Assertion	biimtrrid	⊢ ( 𝜒 → ( 𝜑 → 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		biimtrrid.1	⊢ ( 𝜓 ↔ 𝜑 )
2		biimtrrid.2	⊢ ( 𝜒 → ( 𝜓 → 𝜃 ) )
3	1	biimpri	⊢ ( 𝜑 → 𝜓 )
4	3 2	syl5	⊢ ( 𝜒 → ( 𝜑 → 𝜃 ) )