Description: Contraposition law for polarity. (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2polss.a | |
|
2polss.p | |
||
Assertion | 2polcon4bN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2polss.a | |
|
2 | 2polss.p | |
|
3 | simpl1 | |
|
4 | simp1 | |
|
5 | 1 2 | polssatN | |
6 | 5 | 3adant2 | |
7 | 1 2 | polssatN | |
8 | 4 6 7 | syl2anc | |
9 | 8 | adantr | |
10 | simpr | |
|
11 | 1 2 | polcon3N | |
12 | 3 9 10 11 | syl3anc | |
13 | 12 | ex | |
14 | 1 2 | 3polN | |
15 | 14 | 3adant2 | |
16 | 1 2 | 3polN | |
17 | 16 | 3adant3 | |
18 | 15 17 | sseq12d | |
19 | 13 18 | sylibd | |
20 | simpl1 | |
|
21 | 1 2 | polssatN | |
22 | 21 | 3adant3 | |
23 | 22 | adantr | |
24 | simpr | |
|
25 | 1 2 | polcon3N | |
26 | 20 23 24 25 | syl3anc | |
27 | 26 | ex | |
28 | 19 27 | impbid | |