vtocl3gafOLD

Description: Obsolete version of vtocl3gaf as of 31-May-2025. (Contributed by NM, 10-Aug-2013) (Revised by Mario Carneiro, 11-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	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	vtocl3gafOLD	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )

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	1	nfel1	⊢ Ⅎ 𝑥 𝐴 ∈ 𝑅
15		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝑆
16		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ 𝑇
17	14 15 16	nf3an	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 )
18	17 7	nfim	⊢ Ⅎ 𝑥 ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜓 )
19	2	nfel1	⊢ Ⅎ 𝑦 𝐴 ∈ 𝑅
20	4	nfel1	⊢ Ⅎ 𝑦 𝐵 ∈ 𝑆
21		nfv	⊢ Ⅎ 𝑦 𝑧 ∈ 𝑇
22	19 20 21	nf3an	⊢ Ⅎ 𝑦 ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 )
23	22 8	nfim	⊢ Ⅎ 𝑦 ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜒 )
24	3	nfel1	⊢ Ⅎ 𝑧 𝐴 ∈ 𝑅
25	5	nfel1	⊢ Ⅎ 𝑧 𝐵 ∈ 𝑆
26	6	nfel1	⊢ Ⅎ 𝑧 𝐶 ∈ 𝑇
27	24 25 26	nf3an	⊢ Ⅎ 𝑧 ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 )
28	27 9	nfim	⊢ Ⅎ 𝑧 ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )
29		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑅 ↔ 𝐴 ∈ 𝑅 ) )
30	29	3anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ) )
31	30 10	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜑 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜓 ) ) )
32		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆 ) )
33	32	3anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ) )
34	33 11	imbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜓 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜒 ) ) )
35		eleq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 ∈ 𝑇 ↔ 𝐶 ∈ 𝑇 ) )
36	35	3anbi3d	⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ) )
37	36 12	imbi12d	⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 ) ) )
38	1 2 3 4 5 6 18 23 28 31 34 37 13	vtocl3gf	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 ) )
39	38	pm2.43i	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )

Metamath Proof Explorer

Theorem vtocl3gafOLD

Proof