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

Metamath Proof Explorer

Theorem ee010

Description: e010 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ee010.1	$⊢ φ$
	ee010.2	$⊢ ψ \to χ$
	ee010.3	$⊢ θ$
	ee010.4	$⊢ φ \to (χ \to (θ \to τ))$
Assertion	ee010	$⊢ ψ \to τ$

Proof

Step	Hyp	Ref	Expression
1		ee010.1	$⊢ φ$
2		ee010.2	$⊢ ψ \to χ$
3		ee010.3	$⊢ θ$
4		ee010.4	$⊢ φ \to (χ \to (θ \to τ))$
5	1	a1i	$⊢ ψ \to φ$
6	3	a1i	$⊢ ψ \to θ$
7	5 2 6 4	syl3c	$⊢ ψ \to τ$