Metamath Proof Explorer

Theorem en3lplem1

Description: Lemma for en3lp . (Contributed by Alan Sare, 28-Oct-2011)

Ref Expression
Assertion en3lplem1 ⊢A∈B∧B∈C∧C∈A→x=A→x∩ABC≠∅

Proof

Step Hyp Ref Expression
1 simp3 ⊢A∈B∧B∈C∧C∈A→C∈A
2 eleq2 ⊢x=A→C∈x↔C∈A
3 1 2 syl5ibrcom ⊢A∈B∧B∈C∧C∈A→x=A→C∈x
4 tpid3g ⊢C∈A→C∈ABC
5 4 3ad2ant3 ⊢A∈B∧B∈C∧C∈A→C∈ABC
6 inelcm ⊢C∈x∧C∈ABC→x∩ABC≠∅
7 5 6 sylan2 ⊢C∈x∧A∈B∧B∈C∧C∈A→x∩ABC≠∅
8 7 expcom ⊢A∈B∧B∈C∧C∈A→C∈x→x∩ABC≠∅
9 3 8 syld ⊢A∈B∧B∈C∧C∈A→x=A→x∩ABC≠∅