Metamath Proof Explorer


Theorem ichn

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

Ref Expression
Assertion ichn a b φ a b ¬ φ

Proof

Step Hyp Ref Expression
1 notbi a u b a u b φ φ ¬ a u b a u b φ ¬ φ
2 sbn u b ¬ φ ¬ u b φ
3 2 sbbii b a u b ¬ φ b a ¬ u b φ
4 sbn b a ¬ u b φ ¬ b a u b φ
5 3 4 bitri b a u b ¬ φ ¬ b a u b φ
6 5 sbbii a u b a u b ¬ φ a u ¬ b a u b φ
7 sbn a u ¬ b a u b φ ¬ a u b a u b φ
8 6 7 bitri a u b a u b ¬ φ ¬ a u b a u b φ
9 8 bibi1i a u b a u b ¬ φ ¬ φ ¬ a u b a u b φ ¬ φ
10 1 9 bitr4i a u b a u b φ φ a u b a u b ¬ φ ¬ φ
11 10 2albii a b a u b a u b φ φ a b a u b a u b ¬ φ ¬ φ
12 df-ich a b φ a b a u b a u b φ φ
13 df-ich a b ¬ φ a b a u b a u b ¬ φ ¬ φ
14 11 12 13 3bitr4i a b φ a b ¬ φ