Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf . (Contributed by Alan Sare, 10-Nov-2012) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | sbcg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sbc | |
|
2 | dfclel | |
|
3 | df-clab | |
|
4 | sbv | |
|
5 | 3 4 | bitri | |
6 | 5 | anbi2i | |
7 | 6 | exbii | |
8 | 1 2 7 | 3bitrri | |
9 | dfclel | |
|
10 | 9 | biimpi | |
11 | simpr | |
|
12 | 11 | ax-gen | |
13 | 19.23v | |
|
14 | 13 | biimpi | |
15 | 12 14 | mp1i | |
16 | 2a1 | |
|
17 | 16 | imp | |
18 | 17 | ancrd | |
19 | 18 | eximi | |
20 | 19.37imv | |
|
21 | 19 20 | syl | |
22 | 15 21 | impbid | |
23 | 10 22 | syl | |
24 | 8 23 | bitr3id | |