Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . . 6
β’
β²π¦π |
2 | 1 | sb8ef 2352 |
. . . . 5
β’
(βπ₯π β βπ¦[π¦ / π₯]π) |
3 | | sb8v 2349 |
. . . . 5
β’
(βπ₯π β βπ§[π§ / π₯]π) |
4 | 2, 3 | imbi12i 351 |
. . . 4
β’
((βπ₯π β βπ₯π) β (βπ¦[π¦ / π₯]π β βπ§[π§ / π₯]π)) |
5 | | df-nf 1787 |
. . . 4
β’
(β²π₯π β (βπ₯π β βπ₯π)) |
6 | | pm11.53v 1948 |
. . . 4
β’
(βπ¦βπ§([π¦ / π₯]π β [π§ / π₯]π) β (βπ¦[π¦ / π₯]π β βπ§[π§ / π₯]π)) |
7 | 4, 5, 6 | 3bitr4i 303 |
. . 3
β’
(β²π₯π β βπ¦βπ§([π¦ / π₯]π β [π§ / π₯]π)) |
8 | | nfv 1918 |
. . . . . . 7
β’
β²π§π |
9 | 8 | sb8ef 2352 |
. . . . . 6
β’
(βπ₯π β βπ§[π§ / π₯]π) |
10 | | sb8v 2349 |
. . . . . 6
β’
(βπ₯π β βπ¦[π¦ / π₯]π) |
11 | 9, 10 | imbi12i 351 |
. . . . 5
β’
((βπ₯π β βπ₯π) β (βπ§[π§ / π₯]π β βπ¦[π¦ / π₯]π)) |
12 | | pm11.53v 1948 |
. . . . 5
β’
(βπ§βπ¦([π§ / π₯]π β [π¦ / π₯]π) β (βπ§[π§ / π₯]π β βπ¦[π¦ / π₯]π)) |
13 | 11, 5, 12 | 3bitr4i 303 |
. . . 4
β’
(β²π₯π β βπ§βπ¦([π§ / π₯]π β [π¦ / π₯]π)) |
14 | | alcom 2157 |
. . . 4
β’
(βπ§βπ¦([π§ / π₯]π β [π¦ / π₯]π) β βπ¦βπ§([π§ / π₯]π β [π¦ / π₯]π)) |
15 | 13, 14 | bitri 275 |
. . 3
β’
(β²π₯π β βπ¦βπ§([π§ / π₯]π β [π¦ / π₯]π)) |
16 | 7, 15 | anbi12i 628 |
. 2
β’
((β²π₯π β§ β²π₯π) β (βπ¦βπ§([π¦ / π₯]π β [π§ / π₯]π) β§ βπ¦βπ§([π§ / π₯]π β [π¦ / π₯]π))) |
17 | | pm4.24 565 |
. 2
β’
(β²π₯π β (β²π₯π β§ β²π₯π)) |
18 | | 2albiim 1894 |
. 2
β’
(βπ¦βπ§([π¦ / π₯]π β [π§ / π₯]π) β (βπ¦βπ§([π¦ / π₯]π β [π§ / π₯]π) β§ βπ¦βπ§([π§ / π₯]π β [π¦ / π₯]π))) |
19 | 16, 17, 18 | 3bitr4i 303 |
1
β’
(β²π₯π β βπ¦βπ§([π¦ / π₯]π β [π§ / π₯]π)) |