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

Metamath Proof Explorer

Definition df-vd2

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

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

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