Description: Obsolete version of cbvmow as of 23-May-2024. (Contributed by NM, 9-Mar-1995) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvmowOLD.1 | ||
cbvmowOLD.2 | |||
cbvmowOLD.3 | |||
Assertion | cbvmowOLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvmowOLD.1 | ||
2 | cbvmowOLD.2 | ||
3 | cbvmowOLD.3 | ||
4 | 1 | sb8ev | |
5 | 1 | sb8euv | |
6 | 4 5 | imbi12i | |
7 | moeu | ||
8 | moeu | ||
9 | 6 7 8 | 3bitr4i | |
10 | 2 3 | sbiev | |
11 | 10 | mobii | |
12 | 9 11 | bitri |