Description: Composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbcco3gw when possible. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sbcco3g.1 | |
|
Assertion | sbcco3g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcco3g.1 | |
|
2 | sbcnestg | |
|
3 | elex | |
|
4 | nfcvd | |
|
5 | 4 1 | csbiegf | |
6 | dfsbcq | |
|
7 | 3 5 6 | 3syl | |
8 | 2 7 | bitrd | |