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	⊢ ( 𝜑 → 𝜓 )
	ee10an.2	⊢ 𝜒
	ee10an.3	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion	ee10an	⊢ ( 𝜑 → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		ee10an.1	⊢ ( 𝜑 → 𝜓 )
2		ee10an.2	⊢ 𝜒
3		ee10an.3	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
4	1 2 3	sylancl	⊢ ( 𝜑 → 𝜃 )