Definition df-vd2 38794

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

Assertion

Ref	Expression
df-vd2	|- ( (. ph ,. ps ->. ch ). <-> ( ( ph /\ ps ) -> ch ) )

Detailed syntax breakdown of Definition df-vd2

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

This definition is referenced by:  dfvd2  38795