Description: Setvar variables are interchangeable in a wff they do not appear in. (Contributed by SN, 23-Nov-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | ichv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbv | ||
2 | 1 | sbbii | |
3 | sbv | ||
4 | 2 3 | bitri | |
5 | 4 | sbbii | |
6 | sbv | ||
7 | 5 6 | bitri | |
8 | 7 | gen2 | |
9 | df-ich | ||
10 | 8 9 | mpbir |