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	$$⊢\phi \to \psi$$
	syl2an23an.2	$$⊢\phi \to \chi$$
	syl2an23an.3	$$⊢\left(\theta \wedge \phi \right)\to \tau$$
	syl2an23an.4	$$⊢\left(\psi \wedge \chi \wedge \tau \right)\to \eta$$
Assertion	syl2an23an	$$⊢\left(\theta \wedge \phi \right)\to \eta$$

Proof

Step	Hyp	Ref	Expression
1		syl2an23an.1	$$⊢\phi \to \psi$$
2		syl2an23an.2	$$⊢\phi \to \chi$$
3		syl2an23an.3	$$⊢\left(\theta \wedge \phi \right)\to \tau$$
4		syl2an23an.4	$$⊢\left(\psi \wedge \chi \wedge \tau \right)\to \eta$$
5	1 2 3 4	syl2an3an	$$⊢\left(\phi \wedge \left(\theta \wedge \phi \right)\right)\to \eta$$
6	5	anabss7	$$⊢\left(\theta \wedge \phi \right)\to \eta$$