Metamath Proof Explorer


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 FFilXAFBFAB

Proof

Step Hyp Ref Expression
1 simp1 FFilXAFBFFFilX
2 filin FFilXAFBFABF
3 fileln0 FFilXABFAB
4 1 2 3 syl2anc FFilXAFBFAB