Metamath Proof Explorer

Theorem linerflx2

Description: Reflexivity law for line membership. Part of theorem 6.17 of Schwabhauser p. 45. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	linerflx2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to Q \in (P Line Q)$

Proof

Step	Hyp	Ref	Expression
1		necom	$⊢ P \neq Q \leftrightarrow Q \neq P$
2	1	3anbi3i	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \leftrightarrow (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land Q \neq P)$
3		3ancoma	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land Q \neq P) \leftrightarrow (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \neq P)$
4	2 3	bitri	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \leftrightarrow (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \neq P)$
5		linerflx1	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \neq P)) \to Q \in (Q Line P)$
6	4 5	sylan2b	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to Q \in (Q Line P)$
7		linecom	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Line Q = Q Line P$
8	6 7	eleqtrrd	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to Q \in (P Line Q)$