Description: Composition of two substitutions. Version of sbcco3g with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 27-Nov-2005) (Revised by Gino Giotto, 26-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sbcco3gw.1 | ||
Assertion | sbcco3gw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcco3gw.1 | ||
2 | sbcnestgw | ||
3 | elex | ||
4 | nfcvd | ||
5 | 4 1 | csbiegf | |
6 | dfsbcq | ||
7 | 3 5 6 | 3syl | |
8 | 2 7 | bitrd |