Description: Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbcnestgw when possible. (Contributed by NM, 27-Nov-2005) (Proof shortened by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | sbcnestg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv | |
|
2 | 1 | ax-gen | |
3 | sbcnestgf | |
|
4 | 2 3 | mpan2 | |