Theorem syl2an2

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

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

Proof

Step	Hyp	Ref	Expression
1		syl2an2.1	$$⊢\phi \to \psi$$
2		syl2an2.2	$$⊢\left(\chi \wedge \phi \right)\to \theta$$
3		syl2an2.3	$$⊢\left(\psi \wedge \theta \right)\to \tau$$
4	1	adantl	$$⊢\left(\chi \wedge \phi \right)\to \psi$$
5	4 2 3	syl2anc	$$⊢\left(\chi \wedge \phi \right)\to \tau$$