Metamath Proof Explorer


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 ) )