Metamath Proof Explorer


Theorem iccneg

Description: Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007)

Ref Expression
Assertion iccneg A B C C A B C B A

Proof

Step Hyp Ref Expression
1 renegcl C C
2 ax-1 C C C
3 1 2 impbid2 C C C
4 3 3ad2ant3 A B C C C
5 ancom C B A C A C C B
6 leneg C B C B B C
7 6 ancoms B C C B B C
8 7 3adant1 A B C C B B C
9 leneg A C A C C A
10 9 3adant2 A B C A C C A
11 8 10 anbi12d A B C C B A C B C C A
12 5 11 syl5bbr A B C A C C B B C C A
13 4 12 anbi12d A B C C A C C B C B C C A
14 elicc2 A B C A B C A C C B
15 14 3adant3 A B C C A B C A C C B
16 3anass C A C C B C A C C B
17 15 16 syl6bb A B C C A B C A C C B
18 renegcl B B
19 renegcl A A
20 elicc2 B A C B A C B C C A
21 18 19 20 syl2anr A B C B A C B C C A
22 21 3adant3 A B C C B A C B C C A
23 3anass C B C C A C B C C A
24 22 23 syl6bb A B C C B A C B C C A
25 13 17 24 3bitr4d A B C C A B C B A