Metamath Proof Explorer


Theorem vtocl4ga

Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019) (Proof shortened by Wolf Lammen, 31-May-2025)

Ref Expression
Hypotheses vtocl4ga.1 x = A φ ψ
vtocl4ga.2 y = B ψ χ
vtocl4ga.3 z = C χ ρ
vtocl4ga.4 w = D ρ θ
vtocl4ga.5 x Q y R z S w T φ
Assertion vtocl4ga A Q B R C S D T θ

Proof

Step Hyp Ref Expression
1 vtocl4ga.1 x = A φ ψ
2 vtocl4ga.2 y = B ψ χ
3 vtocl4ga.3 z = C χ ρ
4 vtocl4ga.4 w = D ρ θ
5 vtocl4ga.5 x Q y R z S w T φ
6 3 imbi2d z = C A Q B R χ A Q B R ρ
7 4 imbi2d w = D A Q B R ρ A Q B R θ
8 1 imbi2d x = A z S w T φ z S w T ψ
9 2 imbi2d y = B z S w T ψ z S w T χ
10 5 ex x Q y R z S w T φ
11 8 9 10 vtocl2ga A Q B R z S w T χ
12 11 com12 z S w T A Q B R χ
13 6 7 12 vtocl2ga C S D T A Q B R θ
14 13 impcom A Q B R C S D T θ