Definition df-vd3 38806

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

Assertion

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

Detailed syntax breakdown of Definition df-vd3

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4		wth	. . 3 wff th
5	1, 2, 3, 4	wvd3 38803	. 2 wff (. ph ,. ps ,. ch ->. th ).
6	1, 2, 3	w3a 1037	. . 3 wff ( ph /\ ps /\ ch )
7	6, 4	wi 4	. 2 wff ( ( ph /\ ps /\ ch ) -> th )
8	5, 7	wb 196	1 wff ( (. ph ,. ps ,. ch ->. th ). <-> ( ( ph /\ ps /\ ch ) -> th ) )

This definition is referenced by:  dfvd3  38807