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	|- ( ph -> ps )
	ee10an.2	|- ch
	ee10an.3	|- ( ( ps /\ ch ) -> th )
Assertion	ee10an	|- ( ph -> th )

Proof

Step	Hyp	Ref	Expression
1		ee10an.1	|- ( ph -> ps )
2		ee10an.2	|- ch
3		ee10an.3	|- ( ( ps /\ ch ) -> th )
4	1 2 3	sylancl	|- ( ph -> th )