Theorem syl2anb

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

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

Proof

Step	Hyp	Ref	Expression
1		syl2anb.1	⊢ ( 𝜑 ↔ 𝜓 )
2		syl2anb.2	⊢ ( 𝜏 ↔ 𝜒 )
3		syl2anb.3	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
4	1 3	sylanb	⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜃 )
5	2 4	sylan2b	⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜃 )