Theorem 4cycl2v2nb

Description: In a (maybe degenerate) 4-cycle, two vertice have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017) (Revised by AV, 2-Apr-2021)

	Ref	Expression
Assertion	4cycl2v2nb	$$⊢\left(\left(\left\{A,B\right\}\in E\wedge \left\{B,C\right\}\in E\right)\wedge \left(\left\{C,D\right\}\in E\wedge \left\{D,A\right\}\in E\right)\right)\to \left(\left\{\left\{A,B\right\},\left\{B,C\right\}\right\}\subseteq E\wedge \left\{\left\{A,D\right\},\left\{D,C\right\}\right\}\subseteq E\right)$$

Proof

Step	Hyp	Ref	Expression
1		prssi	$$⊢\left(\left\{A,B\right\}\in E\wedge \left\{B,C\right\}\in E\right)\to \left\{\left\{A,B\right\},\left\{B,C\right\}\right\}\subseteq E$$
2		prcom	$$⊢\left\{D,A\right\}=\left\{A,D\right\}$$
3	2	eleq1i	$$⊢\left\{D,A\right\}\in E\leftrightarrow \left\{A,D\right\}\in E$$
4	3	biimpi	$$⊢\left\{D,A\right\}\in E\to \left\{A,D\right\}\in E$$
5		prcom	$$⊢\left\{C,D\right\}=\left\{D,C\right\}$$
6	5	eleq1i	$$⊢\left\{C,D\right\}\in E\leftrightarrow \left\{D,C\right\}\in E$$
7	6	biimpi	$$⊢\left\{C,D\right\}\in E\to \left\{D,C\right\}\in E$$
8		prssi	$$⊢\left(\left\{A,D\right\}\in E\wedge \left\{D,C\right\}\in E\right)\to \left\{\left\{A,D\right\},\left\{D,C\right\}\right\}\subseteq E$$
9	4 7 8	syl2anr	$$⊢\left(\left\{C,D\right\}\in E\wedge \left\{D,A\right\}\in E\right)\to \left\{\left\{A,D\right\},\left\{D,C\right\}\right\}\subseteq E$$
10	1 9	anim12i	$$⊢\left(\left(\left\{A,B\right\}\in E\wedge \left\{B,C\right\}\in E\right)\wedge \left(\left\{C,D\right\}\in E\wedge \left\{D,A\right\}\in E\right)\right)\to \left(\left\{\left\{A,B\right\},\left\{B,C\right\}\right\}\subseteq E\wedge \left\{\left\{A,D\right\},\left\{D,C\right\}\right\}\subseteq E\right)$$