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 φ , ψ χ φ ψ χ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 wps wff ψ
2 wch wff χ
3 0 1 2 wvd2 wff φ , ψ χ
4 0 1 wa wff φ ψ
5 4 2 wi wff φ ψ χ
6 3 5 wb wff φ , ψ χ φ ψ χ