Theorem ee10an

Description: e10an without virtual deductions. sylancl is also e10an without virtual deductions, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ee10an.1	$$⊢\phi \to \psi$$
2		ee10an.2	$$⊢\chi$$
3		ee10an.3	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
4	1 2 3	sylancl	$$⊢\phi \to \theta$$