Mathbox for Jeff Hankins < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  neiin Structured version   Unicode version

Theorem neiin 26326
 Description: Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.)
Assertion
Ref Expression
neiin

Proof of Theorem neiin
StepHypRef Expression
1 simpr 448 . . . . . . 7
2 simpl 444 . . . . . . . 8
3 eqid 2435 . . . . . . . . 9
43neiss2 17157 . . . . . . . 8
53neii1 17162 . . . . . . . 8
63neiint 17160 . . . . . . . 8
72, 4, 5, 6syl3anc 1184 . . . . . . 7
81, 7mpbid 202 . . . . . 6
9 ssinss1 3561 . . . . . 6
108, 9syl 16 . . . . 5
11103adant3 977 . . . 4
12 inss2 3554 . . . . 5
13 simpr 448 . . . . . . 7
14 simpl 444 . . . . . . . 8
153neiss2 17157 . . . . . . . 8
163neii1 17162 . . . . . . . 8
173neiint 17160 . . . . . . . 8
1814, 15, 16, 17syl3anc 1184 . . . . . . 7
1913, 18mpbid 202 . . . . . 6
20193adant2 976 . . . . 5
2112, 20syl5ss 3351 . . . 4
2211, 21ssind 3557 . . 3
23 simp1 957 . . . 4
2453adant3 977 . . . 4
25163adant2 976 . . . 4
263ntrin 17117 . . . 4
2723, 24, 25, 26syl3anc 1184 . . 3
2822, 27sseqtr4d 3377 . 2
29 ssinss1 3561 . . . . 5
304, 29syl 16 . . . 4
31 ssinss1 3561 . . . . 5
325, 31syl 16 . . . 4
333neiint 17160 . . . 4
342, 30, 32, 33syl3anc 1184 . . 3