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 ( [ 𝑎𝑏 ] 𝜑 ↔ [ 𝑎𝑏 ] ¬ 𝜑 )