Metamath Proof Explorer

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	$⊢ φ \to ψ$
	syl2an23an.2	$⊢ φ \to χ$
	syl2an23an.3	$⊢ (θ \land φ) \to τ$
	syl2an23an.4	$⊢ (ψ \land χ \land τ) \to η$
Assertion	syl2an23an	$⊢ (θ \land φ) \to η$

Proof

Step	Hyp	Ref	Expression
1		syl2an23an.1	$⊢ φ \to ψ$
2		syl2an23an.2	$⊢ φ \to χ$
3		syl2an23an.3	$⊢ (θ \land φ) \to τ$
4		syl2an23an.4	$⊢ (ψ \land χ \land τ) \to η$
5	1 2 3 4	syl2an3an	$⊢ (φ \land (θ \land φ)) \to η$
6	5	anabss7	$⊢ (θ \land φ) \to η$