Theorem syl2anbr

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999)

	Ref	Expression
Hypotheses	syl2anbr.1	⊢ ( 𝜓 ↔ 𝜑 )
	syl2anbr.2	⊢ ( 𝜒 ↔ 𝜏 )
	syl2anbr.3	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion	syl2anbr	⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		syl2anbr.1	⊢ ( 𝜓 ↔ 𝜑 )
2		syl2anbr.2	⊢ ( 𝜒 ↔ 𝜏 )
3		syl2anbr.3	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
4	1 3	sylanbr	⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜃 )
5	2 4	sylan2br	⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜃 )