Metamath Proof Explorer


Definition df-vd1

Description: Definition of virtual deduction. (Contributed by Alan Sare, 21-Apr-2011) (New usage is discouraged.)

Ref Expression
Assertion df-vd1 φψφψ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wffφ
1 wps wffψ
2 0 1 wvd1 wffφψ
3 0 1 wi wffφψ
4 2 3 wb wffφψφψ