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