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

Proof

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