ichexmpl2

Description: Example for interchangeable setvar variables in an arithmetic expression. (Contributed by AV, 31-Jul-2023)

		Ref	Expression
	Assertion	ichexmpl2	$⊢ [a ⇄ b] ((a \in ℂ \land b \in ℂ \land c \in ℂ) \to a^{2} + b^{2} = c^{2})$

Proof

Step	Hyp	Ref	Expression
1		eleq1w	$⊢ a = t \to (a \in ℂ \leftrightarrow t \in ℂ)$
2	1	3anbi1d	$⊢ a = t \to ((a \in ℂ \land b \in ℂ \land c \in ℂ) \leftrightarrow (t \in ℂ \land b \in ℂ \land c \in ℂ))$
3		oveq1	$⊢ a = t \to a^{2} = t^{2}$
4	3	oveq1d	$⊢ a = t \to a^{2} + b^{2} = t^{2} + b^{2}$
5	4	eqeq1d	$⊢ a = t \to (a^{2} + b^{2} = c^{2} \leftrightarrow t^{2} + b^{2} = c^{2})$
6	2 5	imbi12d	$⊢ a = t \to (((a \in ℂ \land b \in ℂ \land c \in ℂ) \to a^{2} + b^{2} = c^{2}) \leftrightarrow ((t \in ℂ \land b \in ℂ \land c \in ℂ) \to t^{2} + b^{2} = c^{2}))$
7		eleq1w	$⊢ b = a \to (b \in ℂ \leftrightarrow a \in ℂ)$
8	7	3anbi2d	$⊢ b = a \to ((t \in ℂ \land b \in ℂ \land c \in ℂ) \leftrightarrow (t \in ℂ \land a \in ℂ \land c \in ℂ))$
9		oveq1	$⊢ b = a \to b^{2} = a^{2}$
10	9	oveq2d	$⊢ b = a \to t^{2} + b^{2} = t^{2} + a^{2}$
11	10	eqeq1d	$⊢ b = a \to (t^{2} + b^{2} = c^{2} \leftrightarrow t^{2} + a^{2} = c^{2})$
12	8 11	imbi12d	$⊢ b = a \to (((t \in ℂ \land b \in ℂ \land c \in ℂ) \to t^{2} + b^{2} = c^{2}) \leftrightarrow ((t \in ℂ \land a \in ℂ \land c \in ℂ) \to t^{2} + a^{2} = c^{2}))$
13		eleq1w	$⊢ t = b \to (t \in ℂ \leftrightarrow b \in ℂ)$
14	13	3anbi1d	$⊢ t = b \to ((t \in ℂ \land a \in ℂ \land c \in ℂ) \leftrightarrow (b \in ℂ \land a \in ℂ \land c \in ℂ))$
15		oveq1	$⊢ t = b \to t^{2} = b^{2}$
16	15	oveq1d	$⊢ t = b \to t^{2} + a^{2} = b^{2} + a^{2}$
17	16	eqeq1d	$⊢ t = b \to (t^{2} + a^{2} = c^{2} \leftrightarrow b^{2} + a^{2} = c^{2})$
18	14 17	imbi12d	$⊢ t = b \to (((t \in ℂ \land a \in ℂ \land c \in ℂ) \to t^{2} + a^{2} = c^{2}) \leftrightarrow ((b \in ℂ \land a \in ℂ \land c \in ℂ) \to b^{2} + a^{2} = c^{2}))$
19		3ancoma	$⊢ (b \in ℂ \land a \in ℂ \land c \in ℂ) \leftrightarrow (a \in ℂ \land b \in ℂ \land c \in ℂ)$
20	19	imbi1i	$⊢ ((b \in ℂ \land a \in ℂ \land c \in ℂ) \to b^{2} + a^{2} = c^{2}) \leftrightarrow ((a \in ℂ \land b \in ℂ \land c \in ℂ) \to b^{2} + a^{2} = c^{2})$
21		sqcl	$⊢ b \in ℂ \to b^{2} \in ℂ$
22	21	3ad2ant2	$⊢ (a \in ℂ \land b \in ℂ \land c \in ℂ) \to b^{2} \in ℂ$
23		sqcl	$⊢ a \in ℂ \to a^{2} \in ℂ$
24	23	3ad2ant1	$⊢ (a \in ℂ \land b \in ℂ \land c \in ℂ) \to a^{2} \in ℂ$
25	22 24	addcomd	$⊢ (a \in ℂ \land b \in ℂ \land c \in ℂ) \to b^{2} + a^{2} = a^{2} + b^{2}$
26	25	eqeq1d	$⊢ (a \in ℂ \land b \in ℂ \land c \in ℂ) \to (b^{2} + a^{2} = c^{2} \leftrightarrow a^{2} + b^{2} = c^{2})$
27	26	pm5.74i	$⊢ ((a \in ℂ \land b \in ℂ \land c \in ℂ) \to b^{2} + a^{2} = c^{2}) \leftrightarrow ((a \in ℂ \land b \in ℂ \land c \in ℂ) \to a^{2} + b^{2} = c^{2})$
28	20 27	bitri	$⊢ ((b \in ℂ \land a \in ℂ \land c \in ℂ) \to b^{2} + a^{2} = c^{2}) \leftrightarrow ((a \in ℂ \land b \in ℂ \land c \in ℂ) \to a^{2} + b^{2} = c^{2})$
29	18 28	bitrdi	$⊢ t = b \to (((t \in ℂ \land a \in ℂ \land c \in ℂ) \to t^{2} + a^{2} = c^{2}) \leftrightarrow ((a \in ℂ \land b \in ℂ \land c \in ℂ) \to a^{2} + b^{2} = c^{2}))$
30	6 12 29	ichcircshi	$⊢ [a ⇄ b] ((a \in ℂ \land b \in ℂ \land c \in ℂ) \to a^{2} + b^{2} = c^{2})$

Metamath Proof Explorer

Theorem ichexmpl2

Proof