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

Metamath Proof Explorer

Theorem a2d

Description: Deduction distributing an embedded antecedent. Deduction form of ax-2 . (Contributed by NM, 23-Jun-1994)

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

Step	Hyp	Ref	Expression
1		a2d.1	$⊢ φ \to (ψ \to (χ \to θ))$
2		ax-2	$⊢ (ψ \to (χ \to θ)) \to ((ψ \to χ) \to (ψ \to θ))$
3	1 2	syl	$⊢ φ \to ((ψ \to χ) \to (ψ \to θ))$