This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtocl3gafOLD

Description: Obsolete version of vtocl3gaf as of 31-May-2025. (Contributed by NM, 10-Aug-2013) (Revised by Mario Carneiro, 11-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtocl3gaf.a 
|- F/_ x A
vtocl3gaf.b 
|- F/_ y A
vtocl3gaf.c 
|- F/_ z A
vtocl3gaf.d 
|- F/_ y B
vtocl3gaf.e 
|- F/_ z B
vtocl3gaf.f 
|- F/_ z C
vtocl3gaf.1 
|- F/ x ps
vtocl3gaf.2 
|- F/ y ch
vtocl3gaf.3 
|- F/ z th
vtocl3gaf.4 
|- ( x = A -> ( ph <-> ps ) )
vtocl3gaf.5 
|- ( y = B -> ( ps <-> ch ) )
vtocl3gaf.6 
|- ( z = C -> ( ch <-> th ) )
vtocl3gaf.7 
|- ( ( x e. R /\ y e. S /\ z e. T ) -> ph )
Assertion vtocl3gafOLD 
|- ( ( A e. R /\ B e. S /\ C e. T ) -> th )

Proof

Step Hyp Ref Expression
1 vtocl3gaf.a 
 |-  F/_ x A
2 vtocl3gaf.b 
 |-  F/_ y A
3 vtocl3gaf.c 
 |-  F/_ z A
4 vtocl3gaf.d 
 |-  F/_ y B
5 vtocl3gaf.e 
 |-  F/_ z B
6 vtocl3gaf.f 
 |-  F/_ z C
7 vtocl3gaf.1 
 |-  F/ x ps
8 vtocl3gaf.2 
 |-  F/ y ch
9 vtocl3gaf.3 
 |-  F/ z th
10 vtocl3gaf.4 
 |-  ( x = A -> ( ph <-> ps ) )
11 vtocl3gaf.5 
 |-  ( y = B -> ( ps <-> ch ) )
12 vtocl3gaf.6 
 |-  ( z = C -> ( ch <-> th ) )
13 vtocl3gaf.7 
 |-  ( ( x e. R /\ y e. S /\ z e. T ) -> ph )
14 1 nfel1 
 |-  F/ x A e. R
15 nfv 
 |-  F/ x y e. S
16 nfv 
 |-  F/ x z e. T
17 14 15 16 nf3an 
 |-  F/ x ( A e. R /\ y e. S /\ z e. T )
18 17 7 nfim 
 |-  F/ x ( ( A e. R /\ y e. S /\ z e. T ) -> ps )
19 2 nfel1 
 |-  F/ y A e. R
20 4 nfel1 
 |-  F/ y B e. S
21 nfv 
 |-  F/ y z e. T
22 19 20 21 nf3an 
 |-  F/ y ( A e. R /\ B e. S /\ z e. T )
23 22 8 nfim 
 |-  F/ y ( ( A e. R /\ B e. S /\ z e. T ) -> ch )
24 3 nfel1 
 |-  F/ z A e. R
25 5 nfel1 
 |-  F/ z B e. S
26 6 nfel1 
 |-  F/ z C e. T
27 24 25 26 nf3an 
 |-  F/ z ( A e. R /\ B e. S /\ C e. T )
28 27 9 nfim 
 |-  F/ z ( ( A e. R /\ B e. S /\ C e. T ) -> th )
29 eleq1 
 |-  ( x = A -> ( x e. R <-> A e. R ) )
30 29 3anbi1d 
 |-  ( x = A -> ( ( x e. R /\ y e. S /\ z e. T ) <-> ( A e. R /\ y e. S /\ z e. T ) ) )
31 30 10 imbi12d 
 |-  ( x = A -> ( ( ( x e. R /\ y e. S /\ z e. T ) -> ph ) <-> ( ( A e. R /\ y e. S /\ z e. T ) -> ps ) ) )
32 eleq1 
 |-  ( y = B -> ( y e. S <-> B e. S ) )
33 32 3anbi2d 
 |-  ( y = B -> ( ( A e. R /\ y e. S /\ z e. T ) <-> ( A e. R /\ B e. S /\ z e. T ) ) )
34 33 11 imbi12d 
 |-  ( y = B -> ( ( ( A e. R /\ y e. S /\ z e. T ) -> ps ) <-> ( ( A e. R /\ B e. S /\ z e. T ) -> ch ) ) )
35 eleq1 
 |-  ( z = C -> ( z e. T <-> C e. T ) )
36 35 3anbi3d 
 |-  ( z = C -> ( ( A e. R /\ B e. S /\ z e. T ) <-> ( A e. R /\ B e. S /\ C e. T ) ) )
37 36 12 imbi12d 
 |-  ( z = C -> ( ( ( A e. R /\ B e. S /\ z e. T ) -> ch ) <-> ( ( A e. R /\ B e. S /\ C e. T ) -> th ) ) )
38 1 2 3 4 5 6 18 23 28 31 34 37 13 vtocl3gf 
 |-  ( ( A e. R /\ B e. S /\ C e. T ) -> ( ( A e. R /\ B e. S /\ C e. T ) -> th ) )
39 38 pm2.43i 
 |-  ( ( A e. R /\ B e. S /\ C e. T ) -> th )