This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to ψ$
	ee10an.2	$⊢ χ$
	ee10an.3	$⊢ (ψ \land χ) \to θ$
Assertion	ee10an	$⊢ φ \to θ$

Proof

Step	Hyp	Ref	Expression
1		ee10an.1	$⊢ φ \to ψ$
2		ee10an.2	$⊢ χ$
3		ee10an.3	$⊢ (ψ \land χ) \to θ$
4	1 2 3	sylancl	$⊢ φ \to θ$