Description: Obsolete version of rexcom as of 8-Dec-2024. (Contributed by NM, 19-Nov-1995) (Revised by Mario Carneiro, 14-Oct-2016) (Proof shortened by BJ, 26-Aug-2023) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | rexcomOLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex | ||
2 | 1 | rexbii | |
3 | rexcom4 | ||
4 | r19.42v | ||
5 | 4 | exbii | |
6 | df-rex | ||
7 | 5 6 | bitr4i | |
8 | 2 3 7 | 3bitri |