Step Hyp Ref
Expression 1 2eu4 2380 . 2
2 nfia1 1954 . . . . . 6
3 nfa1 1897 . . . . . . . . . . . . 13
4 nfv 1707 . . . . . . . . . . . . 13
5 simpl 457 . . . . . . . . . . . . . . 15
6 5 imim2i 14 . . . . . . . . . . . . . 14
7 6 sps 1865 . . . . . . . . . . . . 13
8 3 , 4 , 7 exlimd 1914 . . . . . . . . . . . 12
9 ax12v 1855 . . . . . . . . . . . 12
10 8 , 9 syli 37 . . . . . . . . . . 11
11 10 com12 31 . . . . . . . . . 10
12 11 spsd 1867 . . . . . . . . 9
13 nfs1v 2181 . . . . . . . . . . . . 13
14 simpr 461 . . . . . . . . . . . . . . . 16
15 14 imim2i 14 . . . . . . . . . . . . . . 15
16 sbequ1 1991 . . . . . . . . . . . . . . 15
17 15 , 16 syli 37 . . . . . . . . . . . . . 14
18 17 sps 1865 . . . . . . . . . . . . 13
19 3 , 13 , 18 exlimd 1914 . . . . . . . . . . . 12
20 19 imim2d 52 . . . . . . . . . . 11
21 20 al2imi 1636 . . . . . . . . . 10
22 sb6 2173 . . . . . . . . . . 11
23 2sb6 2188 . . . . . . . . . . 11
24 22 , 23 bitr3i 251 . . . . . . . . . 10
25 21 , 24 syl6ib 226 . . . . . . . . 9
26 12 , 25 sylcom 29 . . . . . . . 8
27 26 ancld 553 . . . . . . 7
28 2albiim 1700 . . . . . . 7
29 27 , 28 syl6ibr 227 . . . . . 6
30 2 , 29 exlimi 1912 . . . . 5
31 30 2eximdv 1712 . . . 4
32 31 imp 429 . . 3
33 bi2 198 . . . . . . 7
34 33 2alimi 1634 . . . . . 6
35 34 2eximi 1657 . . . . 5
36 2exsb 2213 . . . . 5
37 35 , 36 sylibr 212 . . . 4
38 bi1 186 . . . . . 6
39 38 2alimi 1634 . . . . 5
40 39 2eximi 1657 . . . 4
41 37 , 40 jca 532 . . 3
42 32 , 41 impbii 188 . 2
43 1 , 42 bitri 249 1
