ichn

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

		Ref	Expression
	Assertion	ichn	$⊢ [a ⇄ b] φ \leftrightarrow [a ⇄ b] \neg φ$

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

Metamath Proof Explorer