Theorem syl2an3an

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

	Ref	Expression
Hypotheses	syl2an3an.1	$$⊢\phi \to \psi$$
	syl2an3an.2	$$⊢\phi \to \chi$$
	syl2an3an.3	$$⊢\theta \to \tau$$
	syl2an3an.4	$$⊢\left(\psi \wedge \chi \wedge \tau \right)\to \eta$$
Assertion	syl2an3an	$$⊢\left(\phi \wedge \theta \right)\to \eta$$

Proof

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