Theorem icht

Description: A theorem is interchangeable. (Contributed by SN, 4-May-2024)

	Ref	Expression
Hypothesis	icht.1	$$⊢\phi$$
Assertion	icht	$$⊢\left[x\rightleftarrows y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		icht.1	$$⊢\phi$$
2	1	sbt	$$⊢\left[a/y\right]\phi$$
3	2	sbt	$$⊢\left[y/x\right]\left[a/y\right]\phi$$
4	3	sbt	$$⊢\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi$$
5	4 1	2th	$$⊢\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi$$
6	5	gen2	$$⊢\forall x\forall y\left(\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi \right)$$
7		df-ich	$$⊢\left[x\rightleftarrows y\right]\phi \leftrightarrow \forall x\forall y\left(\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi \right)$$
8	6 7	mpbir	$$⊢\left[x\rightleftarrows y\right]\phi$$