Metamath Proof Explorer


Theorem 2polcon4bN

Description: Contraposition law for polarity. (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2polss.a A=AtomsK
2polss.p ˙=𝑃K
Assertion 2polcon4bN KHLXAYA˙˙X˙˙Y˙Y˙X

Proof

Step Hyp Ref Expression
1 2polss.a A=AtomsK
2 2polss.p ˙=𝑃K
3 simpl1 KHLXAYA˙˙X˙˙YKHL
4 simp1 KHLXAYAKHL
5 1 2 polssatN KHLYA˙YA
6 5 3adant2 KHLXAYA˙YA
7 1 2 polssatN KHL˙YA˙˙YA
8 4 6 7 syl2anc KHLXAYA˙˙YA
9 8 adantr KHLXAYA˙˙X˙˙Y˙˙YA
10 simpr KHLXAYA˙˙X˙˙Y˙˙X˙˙Y
11 1 2 polcon3N KHL˙˙YA˙˙X˙˙Y˙˙˙Y˙˙˙X
12 3 9 10 11 syl3anc KHLXAYA˙˙X˙˙Y˙˙˙Y˙˙˙X
13 12 ex KHLXAYA˙˙X˙˙Y˙˙˙Y˙˙˙X
14 1 2 3polN KHLYA˙˙˙Y=˙Y
15 14 3adant2 KHLXAYA˙˙˙Y=˙Y
16 1 2 3polN KHLXA˙˙˙X=˙X
17 16 3adant3 KHLXAYA˙˙˙X=˙X
18 15 17 sseq12d KHLXAYA˙˙˙Y˙˙˙X˙Y˙X
19 13 18 sylibd KHLXAYA˙˙X˙˙Y˙Y˙X
20 simpl1 KHLXAYA˙Y˙XKHL
21 1 2 polssatN KHLXA˙XA
22 21 3adant3 KHLXAYA˙XA
23 22 adantr KHLXAYA˙Y˙X˙XA
24 simpr KHLXAYA˙Y˙X˙Y˙X
25 1 2 polcon3N KHL˙XA˙Y˙X˙˙X˙˙Y
26 20 23 24 25 syl3anc KHLXAYA˙Y˙X˙˙X˙˙Y
27 26 ex KHLXAYA˙Y˙X˙˙X˙˙Y
28 19 27 impbid KHLXAYA˙˙X˙˙Y˙Y˙X