3wlkdlem7

	Ref	Expression
Hypotheses	3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
	3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
	3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
	3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
	3wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L))$
Assertion	3wlkdlem7	$⊢ φ \to (J \in V \land K \in V \land L \in V)$

Step	Hyp	Ref	Expression
1		3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
2		3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
3		3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
4		3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
5		3wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L))$
6	1 2 3 4 5	3wlkdlem6	$⊢ φ \to (A \in I (J) \land B \in I (K) \land C \in I (L))$
7		elfvex	$⊢ A \in I (J) \to J \in V$
8		elfvex	$⊢ B \in I (K) \to K \in V$
9		elfvex	$⊢ C \in I (L) \to L \in V$
10	7 8 9	3anim123i	$⊢ (A \in I (J) \land B \in I (K) \land C \in I (L)) \to (J \in V \land K \in V \land L \in V)$
11	6 10	syl	$⊢ φ \to (J \in V \land K \in V \land L \in V)$

Metamath Proof Explorer