Metamath Proof Explorer


Theorem vtocl3ga

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995) Reduce axiom usage. (Revised by GG, 3-Oct-2024) (Proof shortened by Wolf Lammen, 31-May-2025)

Ref Expression
Hypotheses vtocl3ga.1
|- ( x = A -> ( ph <-> ps ) )
vtocl3ga.2
|- ( y = B -> ( ps <-> ch ) )
vtocl3ga.3
|- ( z = C -> ( ch <-> th ) )
vtocl3ga.4
|- ( ( x e. D /\ y e. R /\ z e. S ) -> ph )
Assertion vtocl3ga
|- ( ( A e. D /\ B e. R /\ C e. S ) -> th )

Proof

Step Hyp Ref Expression
1 vtocl3ga.1
 |-  ( x = A -> ( ph <-> ps ) )
2 vtocl3ga.2
 |-  ( y = B -> ( ps <-> ch ) )
3 vtocl3ga.3
 |-  ( z = C -> ( ch <-> th ) )
4 vtocl3ga.4
 |-  ( ( x e. D /\ y e. R /\ z e. S ) -> ph )
5 3 imbi2d
 |-  ( z = C -> ( ( ( A e. D /\ B e. R ) -> ch ) <-> ( ( A e. D /\ B e. R ) -> th ) ) )
6 1 imbi2d
 |-  ( x = A -> ( ( z e. S -> ph ) <-> ( z e. S -> ps ) ) )
7 2 imbi2d
 |-  ( y = B -> ( ( z e. S -> ps ) <-> ( z e. S -> ch ) ) )
8 4 3expia
 |-  ( ( x e. D /\ y e. R ) -> ( z e. S -> ph ) )
9 6 7 8 vtocl2ga
 |-  ( ( A e. D /\ B e. R ) -> ( z e. S -> ch ) )
10 9 com12
 |-  ( z e. S -> ( ( A e. D /\ B e. R ) -> ch ) )
11 5 10 vtoclga
 |-  ( C e. S -> ( ( A e. D /\ B e. R ) -> th ) )
12 11 impcom
 |-  ( ( ( A e. D /\ B e. R ) /\ C e. S ) -> th )
13 12 3impa
 |-  ( ( A e. D /\ B e. R /\ C e. S ) -> th )