Description: Obsolete version of copsex2g as of 1-Sep-2024. (Contributed by NM, 28-May-1995) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | copsex2g.1 | |
|
Assertion | copsex2gOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | copsex2g.1 | |
|
2 | elisset | |
|
3 | elisset | |
|
4 | exdistrv | |
|
5 | nfe1 | |
|
6 | nfv | |
|
7 | 5 6 | nfbi | |
8 | nfe1 | |
|
9 | 8 | nfex | |
10 | nfv | |
|
11 | 9 10 | nfbi | |
12 | opeq12 | |
|
13 | copsexgw | |
|
14 | 13 | eqcoms | |
15 | 12 14 | syl | |
16 | 15 1 | bitr3d | |
17 | 11 16 | exlimi | |
18 | 7 17 | exlimi | |
19 | 4 18 | sylbir | |
20 | 2 3 19 | syl2an | |