Theorem filinn0

Description: The intersection of two elements of a filter can't be empty. (Contributed by FL, 16-Sep-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	filinn0	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\wedge B\in F\right)\to A\cap B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\wedge B\in F\right)\to F\in \mathrm{Fil}\left(X\right)$$
2		filin	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\wedge B\in F\right)\to A\cap B\in F$$
3		fileln0	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\cap B\in F\right)\to A\cap B\ne \varnothing$$
4	1 2 3	syl2anc	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\wedge B\in F\right)\to A\cap B\ne \varnothing$$