Metamath Proof Explorer

Theorem vtocl3gaf

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013) (Revised by Mario Carneiro, 11-Oct-2016) (Proof shortened by Wolf Lammen, 31-May-2025)

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 vtocl3gaf 
|- ( ( 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 3 nfel1 
 |-  F/ z A e. R
15 5 nfel1 
 |-  F/ z B e. S
16 14 15 nfan 
 |-  F/ z ( A e. R /\ B e. S )
17 16 9 nfim 
 |-  F/ z ( ( A e. R /\ B e. S ) -> th )
18 12 imbi2d 
 |-  ( z = C -> ( ( ( A e. R /\ B e. S ) -> ch ) <-> ( ( A e. R /\ B e. S ) -> th ) ) )
19 nfv 
 |-  F/ x z e. T
20 19 7 nfim 
 |-  F/ x ( z e. T -> ps )
21 nfv 
 |-  F/ y z e. T
22 21 8 nfim 
 |-  F/ y ( z e. T -> ch )
23 10 imbi2d 
 |-  ( x = A -> ( ( z e. T -> ph ) <-> ( z e. T -> ps ) ) )
24 11 imbi2d 
 |-  ( y = B -> ( ( z e. T -> ps ) <-> ( z e. T -> ch ) ) )
25 13 3expia 
 |-  ( ( x e. R /\ y e. S ) -> ( z e. T -> ph ) )
26 1 2 4 20 22 23 24 25 vtocl2gaf 
 |-  ( ( A e. R /\ B e. S ) -> ( z e. T -> ch ) )
27 26 com12 
 |-  ( z e. T -> ( ( A e. R /\ B e. S ) -> ch ) )
28 6 17 18 27 vtoclgaf 
 |-  ( C e. T -> ( ( A e. R /\ B e. S ) -> th ) )
29 28 impcom 
 |-  ( ( ( A e. R /\ B e. S ) /\ C e. T ) -> th )
30 29 3impa 
 |-  ( ( A e. R /\ B e. S /\ C e. T ) -> th )