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	|- ( (. ph ,. ps ->. ch ). <-> ( ( ph /\ ps ) -> ch ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2		wch	|- ch
3	0 1 2	wvd2	|- (. ph ,. ps ->. ch ).
4	0 1	wa	|- ( ph /\ ps )
5	4 2	wi	|- ( ( ph /\ ps ) -> ch )
6	3 5	wb	|- ( (. ph ,. ps ->. ch ). <-> ( ( ph /\ ps ) -> ch ) )