Description: Obsolete version of vtocl3ga as of 3-Oct-2024. (Contributed by NM, 20-Aug-1995) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | vtocl3gaOLD.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
| vtocl3gaOLD.2 | |- ( y = B -> ( ps <-> ch ) ) |
||
| vtocl3gaOLD.3 | |- ( z = C -> ( ch <-> th ) ) |
||
| vtocl3gaOLD.4 | |- ( ( x e. D /\ y e. R /\ z e. S ) -> ph ) |
||
| Assertion | vtocl3gaOLD | |- ( ( A e. D /\ B e. R /\ C e. S ) -> th ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtocl3gaOLD.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
| 2 | vtocl3gaOLD.2 | |- ( y = B -> ( ps <-> ch ) ) |
|
| 3 | vtocl3gaOLD.3 | |- ( z = C -> ( ch <-> th ) ) |
|
| 4 | vtocl3gaOLD.4 | |- ( ( x e. D /\ y e. R /\ z e. S ) -> ph ) |
|
| 5 | nfcv | |- F/_ x A |
|
| 6 | nfcv | |- F/_ y A |
|
| 7 | nfcv | |- F/_ z A |
|
| 8 | nfcv | |- F/_ y B |
|
| 9 | nfcv | |- F/_ z B |
|
| 10 | nfcv | |- F/_ z C |
|
| 11 | nfv | |- F/ x ps |
|
| 12 | nfv | |- F/ y ch |
|
| 13 | nfv | |- F/ z th |
|
| 14 | 5 6 7 8 9 10 11 12 13 1 2 3 4 | vtocl3gaf | |- ( ( A e. D /\ B e. R /\ C e. S ) -> th ) |