Metamath Proof Explorer

Theorem dfvd3

Description: Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	dfvd3	$⊢ (φ, ψ, χ \to θ) \leftrightarrow (φ \to (ψ \to (χ \to θ)))$

Proof

Step	Hyp	Ref	Expression
1		df-vd3	$⊢ (φ, ψ, χ \to θ) \leftrightarrow ((φ \land ψ \land χ) \to θ)$
2		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
3	2	imbi1i	$⊢ ((φ \land ψ \land χ) \to θ) \leftrightarrow (((φ \land ψ) \land χ) \to θ)$
4		impexp	$⊢ (((φ \land ψ) \land χ) \to θ) \leftrightarrow ((φ \land ψ) \to (χ \to θ))$
5	3 4	bitri	$⊢ ((φ \land ψ \land χ) \to θ) \leftrightarrow ((φ \land ψ) \to (χ \to θ))$
6		impexp	$⊢ ((φ \land ψ) \to (χ \to θ)) \leftrightarrow (φ \to (ψ \to (χ \to θ)))$
7	5 6	bitri	$⊢ ((φ \land ψ \land χ) \to θ) \leftrightarrow (φ \to (ψ \to (χ \to θ)))$
8	1 7	bitri	$⊢ (φ, ψ, χ \to θ) \leftrightarrow (φ \to (ψ \to (χ \to θ)))$