Step | Hyp | Ref
| Expression |
1 | | paddssw.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
2 | | paddssw.p |
. . . . . 6
β’ + =
(+πβπΎ) |
3 | 1, 2 | sspadd1 38674 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β π β (π + π)) |
4 | 3 | 3adant3r3 1184 |
. . . 4
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (π + π)) |
5 | | sstr 3989 |
. . . 4
β’ ((π β (π + π) β§ (π + π) β π) β π β π) |
6 | 4, 5 | sylan 580 |
. . 3
β’ (((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π + π) β π) β π β π) |
7 | 6 | ex 413 |
. 2
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π + π) β π β π β π)) |
8 | | simpl 483 |
. . . . 5
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β π΅) |
9 | | simpr2 1195 |
. . . . 5
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
10 | | simpr1 1194 |
. . . . 5
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
11 | 1, 2 | sspadd2 38675 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β π β (π + π)) |
12 | 8, 9, 10, 11 | syl3anc 1371 |
. . . 4
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (π + π)) |
13 | | sstr 3989 |
. . . 4
β’ ((π β (π + π) β§ (π + π) β π) β π β π) |
14 | 12, 13 | sylan 580 |
. . 3
β’ (((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π + π) β π) β π β π) |
15 | 14 | ex 413 |
. 2
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π + π) β π β π β π)) |
16 | 7, 15 | jcad 513 |
1
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π + π) β π β (π β π β§ π β π))) |