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 e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> Q e. ( P Line Q ) )

Proof

Step Hyp Ref Expression
1 necom 
 |-  ( P =/= Q <-> Q =/= P )
2 1 3anbi3i 
 |-  ( ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) <-> ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ Q =/= P ) )
3 3ancoma 
 |-  ( ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ Q =/= P ) <-> ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q =/= P ) )
4 2 3 bitri 
 |-  ( ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) <-> ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q =/= P ) )
5 linerflx1 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q =/= P ) ) -> Q e. ( Q Line P ) )
6 4 5 sylan2b 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> Q e. ( Q Line P ) )
7 linecom 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( P Line Q ) = ( Q Line P ) )
8 6 7 eleqtrrd 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> Q e. ( P Line Q ) )