Description: Obsolete version of elabgt as of 12-Oct-2024. (Contributed by NM, 7-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | elabgtOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv | |
|
2 | nfab1 | |
|
3 | 2 | nfel2 | |
4 | nfv | |
|
5 | 3 4 | nfbi | |
6 | pm5.5 | |
|
7 | 1 5 6 | spcgf | |
8 | abid | |
|
9 | eleq1 | |
|
10 | 8 9 | bitr3id | |
11 | 10 | bibi1d | |
12 | 11 | biimpd | |
13 | 12 | a2i | |
14 | 13 | alimi | |
15 | 7 14 | impel | |