Proof of Theorem sbcomxyyz
Step | Hyp | Ref
| Expression |
1 | | ax-bndl 1399 |
. 2
|
2 | | ax-ial 1427 |
. . . . 5
|
3 | | drsb1 1680 |
. . . . 5
|
4 | 2, 3 | sbbid 1726 |
. . . 4
|
5 | | drsb1 1680 |
. . . 4
|
6 | 4, 5 | bitr3d 179 |
. . 3
|
7 | | sbequ12 1654 |
. . . . . 6
|
8 | 7 | sps 1430 |
. . . . 5
|
9 | | hbae 1606 |
. . . . . 6
|
10 | | sbequ12 1654 |
. . . . . . 7
|
11 | 10 | sps 1430 |
. . . . . 6
|
12 | 9, 11 | sbbid 1726 |
. . . . 5
|
13 | 8, 12 | bitr3d 179 |
. . . 4
|
14 | | df-nf 1350 |
. . . . . 6
|
15 | 14 | albii 1359 |
. . . . 5
|
16 | | ax-ial 1427 |
. . . . . . 7
|
17 | | nfs1v 1815 |
. . . . . . . . . 10
|
18 | 17 | nfsb 1822 |
. . . . . . . . 9
|
19 | 18 | a1i 9 |
. . . . . . . 8
|
20 | 19 | nfrd 1413 |
. . . . . . 7
|
21 | | nfr 1411 |
. . . . . . . . 9
|
22 | | nfnf1 1436 |
. . . . . . . . . . . . 13
|
23 | | nfa1 1434 |
. . . . . . . . . . . . 13
|
24 | 22, 23 | nfan 1457 |
. . . . . . . . . . . 12
|
25 | 24 | nfri 1412 |
. . . . . . . . . . 11
|
26 | | nfs1v 1815 |
. . . . . . . . . . . . 13
|
27 | 26 | a1i 9 |
. . . . . . . . . . . 12
|
28 | 27 | nfrd 1413 |
. . . . . . . . . . 11
|
29 | | sbequ12 1654 |
. . . . . . . . . . . . . . 15
|
30 | 29, 7 | sylan9bb 435 |
. . . . . . . . . . . . . 14
|
31 | 30 | ex 108 |
. . . . . . . . . . . . 13
|
32 | 31 | sps 1430 |
. . . . . . . . . . . 12
|
33 | 32 | adantl 262 |
. . . . . . . . . . 11
|
34 | 25, 28, 33 | sbiedh 1670 |
. . . . . . . . . 10
|
35 | 34 | ex 108 |
. . . . . . . . 9
|
36 | 21, 35 | syld 40 |
. . . . . . . 8
|
37 | 36 | sps 1430 |
. . . . . . 7
|
38 | 16, 20, 37 | sbiedh 1670 |
. . . . . 6
|
39 | 38 | bicomd 129 |
. . . . 5
|
40 | 15, 39 | sylbir 125 |
. . . 4
|
41 | 13, 40 | jaoi 636 |
. . 3
|
42 | 6, 41 | jaoi 636 |
. 2
|
43 | 1, 42 | ax-mp 7 |
1
|