Theorem vtocl3gaf 2923

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.)

Hypotheses

Ref	Expression
vtocl3gaf.a	⊢ ℲxA
vtocl3gaf.b	⊢ ℲyA
vtocl3gaf.c	⊢ ℲzA
vtocl3gaf.d	⊢ ℲyB
vtocl3gaf.e	⊢ ℲzB
vtocl3gaf.f	⊢ ℲzC
vtocl3gaf.1	⊢ Ⅎxψ
vtocl3gaf.2	⊢ Ⅎyχ
vtocl3gaf.3	⊢ Ⅎzθ
vtocl3gaf.4	⊢ (x = A → (φ ↔ ψ))
vtocl3gaf.5	⊢ (y = B → (ψ ↔ χ))
vtocl3gaf.6	⊢ (z = C → (χ ↔ θ))
vtocl3gaf.7	⊢ ((x ∈ R ∧ y ∈ S ∧ z ∈ T) → φ)

Assertion

Ref	Expression
vtocl3gaf	⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → θ)

Distinct variable groups:   x,y,z,R   x,S,y,z   x,T,y,z

Allowed substitution hints:   φ(x,y,z)   ψ(x,y,z)   χ(x,y,z)   θ(x,y,z)   A(x,y,z)   B(x,y,z)   C(x,y,z)

Proof of Theorem vtocl3gaf

Step	Hyp	Ref	Expression
1		vtocl3gaf.a	. . 3 ⊢ ℲxA
2		vtocl3gaf.b	. . 3 ⊢ ℲyA
3		vtocl3gaf.c	. . 3 ⊢ ℲzA
4		vtocl3gaf.d	. . 3 ⊢ ℲyB
5		vtocl3gaf.e	. . 3 ⊢ ℲzB
6		vtocl3gaf.f	. . 3 ⊢ ℲzC
7	1	nfel1 2499	. . . . 5 ⊢ Ⅎx A ∈ R
8		nfv 1619	. . . . 5 ⊢ Ⅎx y ∈ S
9		nfv 1619	. . . . 5 ⊢ Ⅎx z ∈ T
10	7, 8, 9	nf3an 1827	. . . 4 ⊢ Ⅎx(A ∈ R ∧ y ∈ S ∧ z ∈ T)
11		vtocl3gaf.1	. . . 4 ⊢ Ⅎxψ
12	10, 11	nfim 1813	. . 3 ⊢ Ⅎx((A ∈ R ∧ y ∈ S ∧ z ∈ T) → ψ)
13	2	nfel1 2499	. . . . 5 ⊢ Ⅎy A ∈ R
14	4	nfel1 2499	. . . . 5 ⊢ Ⅎy B ∈ S
15		nfv 1619	. . . . 5 ⊢ Ⅎy z ∈ T
16	13, 14, 15	nf3an 1827	. . . 4 ⊢ Ⅎy(A ∈ R ∧ B ∈ S ∧ z ∈ T)
17		vtocl3gaf.2	. . . 4 ⊢ Ⅎyχ
18	16, 17	nfim 1813	. . 3 ⊢ Ⅎy((A ∈ R ∧ B ∈ S ∧ z ∈ T) → χ)
19	3	nfel1 2499	. . . . 5 ⊢ Ⅎz A ∈ R
20	5	nfel1 2499	. . . . 5 ⊢ Ⅎz B ∈ S
21	6	nfel1 2499	. . . . 5 ⊢ Ⅎz C ∈ T
22	19, 20, 21	nf3an 1827	. . . 4 ⊢ Ⅎz(A ∈ R ∧ B ∈ S ∧ C ∈ T)
23		vtocl3gaf.3	. . . 4 ⊢ Ⅎzθ
24	22, 23	nfim 1813	. . 3 ⊢ Ⅎz((A ∈ R ∧ B ∈ S ∧ C ∈ T) → θ)
25		eleq1 2413	. . . . 5 ⊢ (x = A → (x ∈ R ↔ A ∈ R))
26	25	3anbi1d 1256	. . . 4 ⊢ (x = A → ((x ∈ R ∧ y ∈ S ∧ z ∈ T) ↔ (A ∈ R ∧ y ∈ S ∧ z ∈ T)))
27		vtocl3gaf.4	. . . 4 ⊢ (x = A → (φ ↔ ψ))
28	26, 27	imbi12d 311	. . 3 ⊢ (x = A → (((x ∈ R ∧ y ∈ S ∧ z ∈ T) → φ) ↔ ((A ∈ R ∧ y ∈ S ∧ z ∈ T) → ψ)))
29		eleq1 2413	. . . . 5 ⊢ (y = B → (y ∈ S ↔ B ∈ S))
30	29	3anbi2d 1257	. . . 4 ⊢ (y = B → ((A ∈ R ∧ y ∈ S ∧ z ∈ T) ↔ (A ∈ R ∧ B ∈ S ∧ z ∈ T)))
31		vtocl3gaf.5	. . . 4 ⊢ (y = B → (ψ ↔ χ))
32	30, 31	imbi12d 311	. . 3 ⊢ (y = B → (((A ∈ R ∧ y ∈ S ∧ z ∈ T) → ψ) ↔ ((A ∈ R ∧ B ∈ S ∧ z ∈ T) → χ)))
33		eleq1 2413	. . . . 5 ⊢ (z = C → (z ∈ T ↔ C ∈ T))
34	33	3anbi3d 1258	. . . 4 ⊢ (z = C → ((A ∈ R ∧ B ∈ S ∧ z ∈ T) ↔ (A ∈ R ∧ B ∈ S ∧ C ∈ T)))
35		vtocl3gaf.6	. . . 4 ⊢ (z = C → (χ ↔ θ))
36	34, 35	imbi12d 311	. . 3 ⊢ (z = C → (((A ∈ R ∧ B ∈ S ∧ z ∈ T) → χ) ↔ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → θ)))
37		vtocl3gaf.7	. . 3 ⊢ ((x ∈ R ∧ y ∈ S ∧ z ∈ T) → φ)
38	1, 2, 3, 4, 5, 6, 12, 18, 24, 28, 32, 36, 37	vtocl3gf 2917	. 2 ⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → θ))
39	38	pm2.43i 43	1 ⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → θ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ w3a 934  Ⅎwnf 1544   = wceq 1642   ∈ wcel 1710  Ⅎwnfc 2476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861

This theorem is referenced by:  vtocl3ga  2924