Metamath Proof Explorer


Theorem icccntri

Description: Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses icccntri.1 A
icccntri.2 B
icccntri.3 R+
icccntri.4 AR=C
icccntri.5 BR=D
Assertion icccntri XABXRCD

Proof

Step Hyp Ref Expression
1 icccntri.1 A
2 icccntri.2 B
3 icccntri.3 R+
4 icccntri.4 AR=C
5 icccntri.5 BR=D
6 iccssre ABAB
7 1 2 6 mp2an AB
8 7 sseli XABX
9 4 5 icccntr ABXR+XABXRCD
10 1 2 9 mpanl12 XR+XABXRCD
11 3 10 mpan2 XXABXRCD
12 11 biimpd XXABXRCD
13 8 12 mpcom XABXRCD