This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ichn

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

Ref Expression
Assertion ichn ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ [ 𝑎 ⇄ 𝑏 ] ¬ 𝜑 )

Proof

Step Hyp Ref Expression
1 notbi ⊢ ( ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) ↔ ( ¬ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ ¬ 𝜑 ) )
2 sbn ⊢ ( [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ [ 𝑢 / 𝑏 ] 𝜑 )
3 2 sbbii ⊢ ( [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ [ 𝑏 / 𝑎 ] ¬ [ 𝑢 / 𝑏 ] 𝜑 )
4 sbn ⊢ ( [ 𝑏 / 𝑎 ] ¬ [ 𝑢 / 𝑏 ] 𝜑 ↔ ¬ [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
5 3 4 bitri ⊢ ( [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
6 5 sbbii ⊢ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ [ 𝑎 / 𝑢 ] ¬ [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
7 sbn ⊢ ( [ 𝑎 / 𝑢 ] ¬ [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ ¬ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
8 6 7 bitri ⊢ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
9 8 bibi1i ⊢ ( ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ 𝜑 ) ↔ ( ¬ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ ¬ 𝜑 ) )
10 1 9 bitr4i ⊢ ( ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) ↔ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ 𝜑 ) )
11 10 2albii ⊢ ( ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ 𝜑 ) )
12 df-ich ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
13 df-ich ⊢ ( [ 𝑎 ⇄ 𝑏 ] ¬ 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ 𝜑 ) )
14 11 12 13 3bitr4i ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ [ 𝑎 ⇄ 𝑏 ] ¬ 𝜑 )