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	⊢ Ⅎ 𝑥 𝐴
	vtocl3gaf.b	⊢ Ⅎ 𝑦 𝐴
	vtocl3gaf.c	⊢ Ⅎ 𝑧 𝐴
	vtocl3gaf.d	⊢ Ⅎ 𝑦 𝐵
	vtocl3gaf.e	⊢ Ⅎ 𝑧 𝐵
	vtocl3gaf.f	⊢ Ⅎ 𝑧 𝐶
	vtocl3gaf.1	⊢ Ⅎ 𝑥 𝜓
	vtocl3gaf.2	⊢ Ⅎ 𝑦 𝜒
	vtocl3gaf.3	⊢ Ⅎ 𝑧 𝜃
	vtocl3gaf.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	vtocl3gaf.5	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	vtocl3gaf.6	⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
	vtocl3gaf.7	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜑 )
Assertion	vtocl3gaf	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		vtocl3gaf.a	⊢ Ⅎ 𝑥 𝐴
2		vtocl3gaf.b	⊢ Ⅎ 𝑦 𝐴
3		vtocl3gaf.c	⊢ Ⅎ 𝑧 𝐴
4		vtocl3gaf.d	⊢ Ⅎ 𝑦 𝐵
5		vtocl3gaf.e	⊢ Ⅎ 𝑧 𝐵
6		vtocl3gaf.f	⊢ Ⅎ 𝑧 𝐶
7		vtocl3gaf.1	⊢ Ⅎ 𝑥 𝜓
8		vtocl3gaf.2	⊢ Ⅎ 𝑦 𝜒
9		vtocl3gaf.3	⊢ Ⅎ 𝑧 𝜃
10		vtocl3gaf.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
11		vtocl3gaf.5	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
12		vtocl3gaf.6	⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
13		vtocl3gaf.7	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜑 )
14	3	nfel1	⊢ Ⅎ 𝑧 𝐴 ∈ 𝑅
15	5	nfel1	⊢ Ⅎ 𝑧 𝐵 ∈ 𝑆
16	14 15	nfan	⊢ Ⅎ 𝑧 ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 )
17	16 9	nfim	⊢ Ⅎ 𝑧 ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜃 )
18	12	imbi2d	⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜃 ) ) )
19		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ 𝑇
20	19 7	nfim	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝑇 → 𝜓 )
21		nfv	⊢ Ⅎ 𝑦 𝑧 ∈ 𝑇
22	21 8	nfim	⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝑇 → 𝜒 )
23	10	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 ∈ 𝑇 → 𝜑 ) ↔ ( 𝑧 ∈ 𝑇 → 𝜓 ) ) )
24	11	imbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 ∈ 𝑇 → 𝜓 ) ↔ ( 𝑧 ∈ 𝑇 → 𝜒 ) ) )
25	13	3expia	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑇 → 𝜑 ) )
26	1 2 4 20 22 23 24 25	vtocl2gaf	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑇 → 𝜒 ) )
27	26	com12	⊢ ( 𝑧 ∈ 𝑇 → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜒 ) )
28	6 17 18 27	vtoclgaf	⊢ ( 𝐶 ∈ 𝑇 → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜃 ) )
29	28	impcom	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )
30	29	3impa	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )