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