Metamath Proof Explorer

Theorem ichn

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

Ref Expression
Assertion ichn 
|- ( [ a <> b ] ph <-> [ a <> b ] -. ph )

Proof

Step Hyp Ref Expression
1 notbi 
 |-  ( ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) <-> ( -. [ a / u ] [ b / a ] [ u / b ] ph <-> -. ph ) )
2 sbn 
 |-  ( [ u / b ] -. ph <-> -. [ u / b ] ph )
3 2 sbbii 
 |-  ( [ b / a ] [ u / b ] -. ph <-> [ b / a ] -. [ u / b ] ph )
4 sbn 
 |-  ( [ b / a ] -. [ u / b ] ph <-> -. [ b / a ] [ u / b ] ph )
5 3 4 bitri 
 |-  ( [ b / a ] [ u / b ] -. ph <-> -. [ b / a ] [ u / b ] ph )
6 5 sbbii 
 |-  ( [ a / u ] [ b / a ] [ u / b ] -. ph <-> [ a / u ] -. [ b / a ] [ u / b ] ph )
7 sbn 
 |-  ( [ a / u ] -. [ b / a ] [ u / b ] ph <-> -. [ a / u ] [ b / a ] [ u / b ] ph )
8 6 7 bitri 
 |-  ( [ a / u ] [ b / a ] [ u / b ] -. ph <-> -. [ a / u ] [ b / a ] [ u / b ] ph )
9 8 bibi1i 
 |-  ( ( [ a / u ] [ b / a ] [ u / b ] -. ph <-> -. ph ) <-> ( -. [ a / u ] [ b / a ] [ u / b ] ph <-> -. ph ) )
10 1 9 bitr4i 
 |-  ( ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) <-> ( [ a / u ] [ b / a ] [ u / b ] -. ph <-> -. ph ) )
11 10 2albii 
 |-  ( A. a A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) <-> A. a A. b ( [ a / u ] [ b / a ] [ u / b ] -. ph <-> -. ph ) )
12 df-ich 
 |-  ( [ a <> b ] ph <-> A. a A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) )
13 df-ich 
 |-  ( [ a <> b ] -. ph <-> A. a A. b ( [ a / u ] [ b / a ] [ u / b ] -. ph <-> -. ph ) )
14 11 12 13 3bitr4i 
 |-  ( [ a <> b ] ph <-> [ a <> b ] -. ph )