Theorem syl2an23an

Description: Deduction related to syl3an with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016) (Proof shortened by Wolf Lammen, 28-Jun-2022)

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

Proof

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