Theorem ichn

Description: Negation does not affect interchangeability. (Contributed by SN, 30-Aug-2023)

	Ref	Expression
Assertion	ichn	$$⊢\left[a\rightleftarrows b\right]\phi \leftrightarrow \left[a\rightleftarrows b\right]\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		notbi	$$⊢\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\leftrightarrow \left(\neg \left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \neg \phi \right)$$
2		sbn	$$⊢\left[u/b\right]\neg \phi \leftrightarrow \neg \left[u/b\right]\phi$$
3	2	sbbii	$$⊢\left[b/a\right]\left[u/b\right]\neg \phi \leftrightarrow \left[b/a\right]\neg \left[u/b\right]\phi$$
4		sbn	$$⊢\left[b/a\right]\neg \left[u/b\right]\phi \leftrightarrow \neg \left[b/a\right]\left[u/b\right]\phi$$
5	3 4	bitri	$$⊢\left[b/a\right]\left[u/b\right]\neg \phi \leftrightarrow \neg \left[b/a\right]\left[u/b\right]\phi$$
6	5	sbbii	$$⊢\left[a/u\right]\left[b/a\right]\left[u/b\right]\neg \phi \leftrightarrow \left[a/u\right]\neg \left[b/a\right]\left[u/b\right]\phi$$
7		sbn	$$⊢\left[a/u\right]\neg \left[b/a\right]\left[u/b\right]\phi \leftrightarrow \neg \left[a/u\right]\left[b/a\right]\left[u/b\right]\phi$$
8	6 7	bitri	$$⊢\left[a/u\right]\left[b/a\right]\left[u/b\right]\neg \phi \leftrightarrow \neg \left[a/u\right]\left[b/a\right]\left[u/b\right]\phi$$
9	8	bibi1i	$$⊢\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\neg \phi \leftrightarrow \neg \phi \right)\leftrightarrow \left(\neg \left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \neg \phi \right)$$
10	1 9	bitr4i	$$⊢\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\leftrightarrow \left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\neg \phi \leftrightarrow \neg \phi \right)$$
11	10	2albii	$$⊢\forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)\leftrightarrow \forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\neg \phi \leftrightarrow \neg \phi \right)$$
12		df-ich	$$⊢\left[a\rightleftarrows b\right]\phi \leftrightarrow \forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\phi \leftrightarrow \phi \right)$$
13		df-ich	$$⊢\left[a\rightleftarrows b\right]\neg \phi \leftrightarrow \forall a\forall b\left(\left[a/u\right]\left[b/a\right]\left[u/b\right]\neg \phi \leftrightarrow \neg \phi \right)$$
14	11 12 13	3bitr4i	$$⊢\left[a\rightleftarrows b\right]\phi \leftrightarrow \left[a\rightleftarrows b\right]\neg \phi$$