Metamath Proof Explorer

Definition df-vd3

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

		Ref	Expression
	Assertion	df-vd3	$⊢ (φ, ψ, χ \to θ) \leftrightarrow ((φ \land ψ \land χ) \to θ)$

Step	Hyp	Ref	Expression
0		wph	$wff φ$
1		wps	$wff ψ$
2		wch	$wff χ$
3		wth	$wff θ$
4	0 1 2 3	wvd3	$wff (φ, ψ, χ \to θ)$
5	0 1 2	w3a	$wff (φ \land ψ \land χ)$
6	5 3	wi	$wff ((φ \land ψ \land χ) \to θ)$
7	4 6	wb	$wff ((φ, ψ, χ \to θ) \leftrightarrow ((φ \land ψ \land χ) \to θ))$