Description: Obsolete version of cbvabw as of 23-May-2024. (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvabw.1 | ||
cbvabw.2 | |||
cbvabw.3 | |||
Assertion | cbvabwOLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvabw.1 | ||
2 | cbvabw.2 | ||
3 | cbvabw.3 | ||
4 | 1 | sbco2v | |
5 | 2 3 | sbiev | |
6 | 5 | sbbii | |
7 | 4 6 | bitr3i | |
8 | df-clab | ||
9 | df-clab | ||
10 | 7 8 9 | 3bitr4i | |
11 | 10 | eqriv |