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

Metamath Proof Explorer

Theorem ee110

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

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

Proof

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