Definition df-vd3

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

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

Detailed syntax breakdown

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