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 )