Theorem syl2an3an

Description: syl3an with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016)

	Ref	Expression
Hypotheses	syl2an3an.1	⊢ ( 𝜑 → 𝜓 )
	syl2an3an.2	⊢ ( 𝜑 → 𝜒 )
	syl2an3an.3	⊢ ( 𝜃 → 𝜏 )
	syl2an3an.4	⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜏 ) → 𝜂 )
Assertion	syl2an3an	⊢ ( ( 𝜑 ∧ 𝜃 ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		syl2an3an.1	⊢ ( 𝜑 → 𝜓 )
2		syl2an3an.2	⊢ ( 𝜑 → 𝜒 )
3		syl2an3an.3	⊢ ( 𝜃 → 𝜏 )
4		syl2an3an.4	⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜏 ) → 𝜂 )
5	1 2 3 4	syl3an	⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝜃 ) → 𝜂 )
6	5	3anidm12	⊢ ( ( 𝜑 ∧ 𝜃 ) → 𝜂 )