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 ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → Q ∈ P Line Q

Proof

Step Hyp Ref Expression
1 necom ⊢ P ≠ Q ↔ Q ≠ P
2 1 3anbi3i ⊢ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ↔ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ Q ≠ P
3 3ancoma ⊢ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ Q ≠ P ↔ Q ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ Q ≠ P
4 2 3 bitri ⊢ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ↔ Q ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ Q ≠ P
5 linerflx1 ⊢ N ∈ ℕ ∧ Q ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ Q ≠ P → Q ∈ Q Line P
6 4 5 sylan2b ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → Q ∈ Q Line P
7 linecom ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P Line Q = Q Line P
8 6 7 eleqtrrd ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → Q ∈ P Line Q