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

Metamath Proof Explorer

Theorem 2a1dd

Description: Double deduction introducing two antecedents. Two applications of 2a1dd . Deduction associated with 2a1d . Double deduction associated with 2a1 and 2a1i . (Contributed by Jeff Hankins, 5-Aug-2009)

		Ref	Expression
	Hypothesis	2a1dd.1	$⊢ φ \to (ψ \to χ)$
	Assertion	2a1dd	$⊢ φ \to (ψ \to (θ \to (τ \to χ)))$

Proof

Step	Hyp	Ref	Expression
1		2a1dd.1	$⊢ φ \to (ψ \to χ)$
2	1	a1dd	$⊢ φ \to (ψ \to (τ \to χ))$
3	2	a1dd	$⊢ φ \to (ψ \to (θ \to (τ \to χ)))$