vtocl3gaf

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

	Ref	Expression
Hypotheses	vtocl3gaf.a	$⊢ \underline{Ⅎ} x A$
	vtocl3gaf.b	$⊢ \underline{Ⅎ} y A$
	vtocl3gaf.c	$⊢ \underline{Ⅎ} z A$
	vtocl3gaf.d	$⊢ \underline{Ⅎ} y B$
	vtocl3gaf.e	$⊢ \underline{Ⅎ} z B$
	vtocl3gaf.f	$⊢ \underline{Ⅎ} z C$
	vtocl3gaf.1	$⊢ Ⅎ x ψ$
	vtocl3gaf.2	$⊢ Ⅎ y χ$
	vtocl3gaf.3	$⊢ Ⅎ z θ$
	vtocl3gaf.4	$⊢ x = A \to (φ \leftrightarrow ψ)$
	vtocl3gaf.5	$⊢ y = B \to (ψ \leftrightarrow χ)$
	vtocl3gaf.6	$⊢ z = C \to (χ \leftrightarrow θ)$
	vtocl3gaf.7	$⊢ (x \in R \land y \in S \land z \in T) \to φ$
Assertion	vtocl3gaf	$⊢ (A \in R \land B \in S \land C \in T) \to θ$

Proof

Step	Hyp	Ref	Expression
1		vtocl3gaf.a	$⊢ \underline{Ⅎ} x A$
2		vtocl3gaf.b	$⊢ \underline{Ⅎ} y A$
3		vtocl3gaf.c	$⊢ \underline{Ⅎ} z A$
4		vtocl3gaf.d	$⊢ \underline{Ⅎ} y B$
5		vtocl3gaf.e	$⊢ \underline{Ⅎ} z B$
6		vtocl3gaf.f	$⊢ \underline{Ⅎ} z C$
7		vtocl3gaf.1	$⊢ Ⅎ x ψ$
8		vtocl3gaf.2	$⊢ Ⅎ y χ$
9		vtocl3gaf.3	$⊢ Ⅎ z θ$
10		vtocl3gaf.4	$⊢ x = A \to (φ \leftrightarrow ψ)$
11		vtocl3gaf.5	$⊢ y = B \to (ψ \leftrightarrow χ)$
12		vtocl3gaf.6	$⊢ z = C \to (χ \leftrightarrow θ)$
13		vtocl3gaf.7	$⊢ (x \in R \land y \in S \land z \in T) \to φ$
14	1	nfel1	$⊢ Ⅎ x A \in R$
15		nfv	$⊢ Ⅎ x y \in S$
16		nfv	$⊢ Ⅎ x z \in T$
17	14 15 16	nf3an	$⊢ Ⅎ x (A \in R \land y \in S \land z \in T)$
18	17 7	nfim	$⊢ Ⅎ x ((A \in R \land y \in S \land z \in T) \to ψ)$
19	2	nfel1	$⊢ Ⅎ y A \in R$
20	4	nfel1	$⊢ Ⅎ y B \in S$
21		nfv	$⊢ Ⅎ y z \in T$
22	19 20 21	nf3an	$⊢ Ⅎ y (A \in R \land B \in S \land z \in T)$
23	22 8	nfim	$⊢ Ⅎ y ((A \in R \land B \in S \land z \in T) \to χ)$
24	3	nfel1	$⊢ Ⅎ z A \in R$
25	5	nfel1	$⊢ Ⅎ z B \in S$
26	6	nfel1	$⊢ Ⅎ z C \in T$
27	24 25 26	nf3an	$⊢ Ⅎ z (A \in R \land B \in S \land C \in T)$
28	27 9	nfim	$⊢ Ⅎ z ((A \in R \land B \in S \land C \in T) \to θ)$
29		eleq1	$⊢ x = A \to (x \in R \leftrightarrow A \in R)$
30	29	3anbi1d	$⊢ x = A \to ((x \in R \land y \in S \land z \in T) \leftrightarrow (A \in R \land y \in S \land z \in T))$
31	30 10	imbi12d	$⊢ x = A \to (((x \in R \land y \in S \land z \in T) \to φ) \leftrightarrow ((A \in R \land y \in S \land z \in T) \to ψ))$
32		eleq1	$⊢ y = B \to (y \in S \leftrightarrow B \in S)$
33	32	3anbi2d	$⊢ y = B \to ((A \in R \land y \in S \land z \in T) \leftrightarrow (A \in R \land B \in S \land z \in T))$
34	33 11	imbi12d	$⊢ y = B \to (((A \in R \land y \in S \land z \in T) \to ψ) \leftrightarrow ((A \in R \land B \in S \land z \in T) \to χ))$
35		eleq1	$⊢ z = C \to (z \in T \leftrightarrow C \in T)$
36	35	3anbi3d	$⊢ z = C \to ((A \in R \land B \in S \land z \in T) \leftrightarrow (A \in R \land B \in S \land C \in T))$
37	36 12	imbi12d	$⊢ z = C \to (((A \in R \land B \in S \land z \in T) \to χ) \leftrightarrow ((A \in R \land B \in S \land C \in T) \to θ))$
38	1 2 3 4 5 6 18 23 28 31 34 37 13	vtocl3gf	$⊢ (A \in R \land B \in S \land C \in T) \to ((A \in R \land B \in S \land C \in T) \to θ)$
39	38	pm2.43i	$⊢ (A \in R \land B \in S \land C \in T) \to θ$

Metamath Proof Explorer

Theorem vtocl3gaf

Proof