Step | Hyp | Ref
| Expression |
1 | | simpl1 1188 |
. . . . 5
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β πΎ β π΅) |
2 | | simpl2 1189 |
. . . . 5
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π΄) |
3 | | sstr 3985 |
. . . . . . . 8
β’ ((π β π β§ π β π΄) β π β π΄) |
4 | 3 | ancoms 458 |
. . . . . . 7
β’ ((π β π΄ β§ π β π) β π β π΄) |
5 | 4 | ad2ant2l 743 |
. . . . . 6
β’ (((π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π΄) |
6 | 5 | 3adantl1 1163 |
. . . . 5
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π΄) |
7 | 1, 2, 6 | 3jca 1125 |
. . . 4
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β (πΎ β π΅ β§ π β π΄ β§ π β π΄)) |
8 | | simprl 768 |
. . . 4
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π) |
9 | | padd0.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
10 | | padd0.p |
. . . . 5
β’ + =
(+πβπΎ) |
11 | 9, 10 | paddss1 39201 |
. . . 4
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β (π β π β (π + π) β (π + π))) |
12 | 7, 8, 11 | sylc 65 |
. . 3
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β (π + π) β (π + π)) |
13 | 9, 10 | paddss2 39202 |
. . . . . 6
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β (π β π β (π + π) β (π + π))) |
14 | 13 | 3com23 1123 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β (π β π β (π + π) β (π + π))) |
15 | 14 | imp 406 |
. . . 4
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ π β π) β (π + π) β (π + π)) |
16 | 15 | adantrl 713 |
. . 3
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β (π + π) β (π + π)) |
17 | 12, 16 | sstrd 3987 |
. 2
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β (π + π) β (π + π)) |
18 | 17 | ex 412 |
1
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β ((π β π β§ π β π) β (π + π) β (π + π))) |