Description: Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbcnestgfw when possible. (Contributed by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | sbcnestgf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq | |
|
2 | csbeq1 | |
|
3 | 2 | sbceq1d | |
4 | 1 3 | bibi12d | |
5 | 4 | imbi2d | |
6 | vex | |
|
7 | 6 | a1i | |
8 | csbeq1a | |
|
9 | 8 | sbceq1d | |
10 | 9 | adantl | |
11 | nfnf1 | |
|
12 | 11 | nfal | |
13 | nfa1 | |
|
14 | nfcsb1v | |
|
15 | 14 | a1i | |
16 | sp | |
|
17 | 13 15 16 | nfsbcd | |
18 | 7 10 12 17 | sbciedf | |
19 | 5 18 | vtoclg | |
20 | 19 | imp | |