Description: Obsolete version of cbveuw as of 23-May-2024. (Contributed by NM, 25-Nov-1994) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbveuwOLD.1 | |
|
cbveuwOLD.2 | |
||
cbveuwOLD.3 | |
||
Assertion | cbveuwOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbveuwOLD.1 | |
|
2 | cbveuwOLD.2 | |
|
3 | cbveuwOLD.3 | |
|
4 | 1 | sb8euv | |
5 | 2 3 | sbiev | |
6 | 5 | eubii | |
7 | 4 6 | bitri | |