Step | Hyp | Ref
| Expression |
1 | | pssnel 4039 |
. . . . . . 7
|
2 | 1 | 3ad2ant3 1084 |
. . . . . 6
|
3 | | mrieqvd.1 |
. . . . . . . . . 10
Moore |
4 | 3 | 3ad2ant1 1082 |
. . . . . . . . 9
Moore |
5 | 4 | adantr 481 |
. . . . . . . 8
Moore |
6 | | mrieqvd.2 |
. . . . . . . 8
mrCls |
7 | | simprr 796 |
. . . . . . . . . 10
|
8 | | difsnb 4337 |
. . . . . . . . . 10
|
9 | 7, 8 | sylib 208 |
. . . . . . . . 9
|
10 | | simpl3 1066 |
. . . . . . . . . . 11
|
11 | 10 | pssssd 3704 |
. . . . . . . . . 10
|
12 | 11 | ssdifd 3746 |
. . . . . . . . 9
|
13 | 9, 12 | eqsstr3d 3640 |
. . . . . . . 8
|
14 | | mrieqvd.3 |
. . . . . . . . . 10
mrInd |
15 | | simpl2 1065 |
. . . . . . . . . 10
|
16 | 14, 5, 15 | mrissd 16296 |
. . . . . . . . 9
|
17 | 16 | ssdifssd 3748 |
. . . . . . . 8
|
18 | 5, 6, 13, 17 | mrcssd 16284 |
. . . . . . 7
|
19 | | difssd 3738 |
. . . . . . . . 9
|
20 | 5, 6, 19, 16 | mrcssd 16284 |
. . . . . . . 8
|
21 | 5, 6, 16 | mrcssidd 16285 |
. . . . . . . . 9
|
22 | | simprl 794 |
. . . . . . . . 9
|
23 | 21, 22 | sseldd 3604 |
. . . . . . . 8
|
24 | 6, 14, 5, 15, 22 | ismri2dad 16297 |
. . . . . . . 8
|
25 | 20, 23, 24 | ssnelpssd 3719 |
. . . . . . 7
|
26 | 18, 25 | sspsstrd 3715 |
. . . . . 6
|
27 | 2, 26 | exlimddv 1863 |
. . . . 5
|
28 | 27 | 3expia 1267 |
. . . 4
|
29 | 28 | alrimiv 1855 |
. . 3
|
30 | 29 | ex 450 |
. 2
|
31 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
Moore |
32 | 31 | elfvexd 6222 |
. . . . . . . . . . . . 13
|
33 | | mrieqvd.4 |
. . . . . . . . . . . . . 14
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . 13
|
35 | 32, 34 | ssexd 4805 |
. . . . . . . . . . . 12
|
36 | | difexg 4808 |
. . . . . . . . . . . 12
|
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
|
38 | | simp1r 1086 |
. . . . . . . . . . . . . . . 16
|
39 | | difsnpss 4338 |
. . . . . . . . . . . . . . . 16
|
40 | 38, 39 | sylib 208 |
. . . . . . . . . . . . . . 15
|
41 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | psseq1d 3699 |
. . . . . . . . . . . . . . 15
|
43 | 40, 42 | mpbird 247 |
. . . . . . . . . . . . . 14
|
44 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
45 | 43, 44 | mpd 15 |
. . . . . . . . . . . . 13
|
46 | 41 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
47 | 46 | psseq1d 3699 |
. . . . . . . . . . . . 13
|
48 | 45, 47 | mpbid 222 |
. . . . . . . . . . . 12
|
49 | 48 | 3expia 1267 |
. . . . . . . . . . 11
|
50 | 37, 49 | spcimdv 3290 |
. . . . . . . . . 10
|
51 | 50 | 3impia 1261 |
. . . . . . . . 9
|
52 | 51 | pssned 3705 |
. . . . . . . 8
|
53 | 52 | 3com23 1271 |
. . . . . . 7
|
54 | 3 | 3ad2ant1 1082 |
. . . . . . . . 9
Moore |
55 | 33 | 3ad2ant1 1082 |
. . . . . . . . 9
|
56 | | simp3 1063 |
. . . . . . . . 9
|
57 | 54, 6, 55, 56 | mrieqvlemd 16289 |
. . . . . . . 8
|
58 | 57 | necon3bbid 2831 |
. . . . . . 7
|
59 | 53, 58 | mpbird 247 |
. . . . . 6
|
60 | 59 | 3expia 1267 |
. . . . 5
|
61 | 60 | ralrimiv 2965 |
. . . 4
|
62 | 61 | ex 450 |
. . 3
|
63 | 6, 14, 3, 33 | ismri2d 16293 |
. . 3
|
64 | 62, 63 | sylibrd 249 |
. 2
|
65 | 30, 64 | impbid 202 |
1
|