Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  oppne3 Structured version   Visualization version   Unicode version

Theorem oppne3 24864
 Description: Points lying on opposite sides of a line cannot be equal. (Contributed by Thierry Arnoux, 3-Aug-2020.)
Hypotheses
Ref Expression
hpg.p
hpg.d
hpg.i Itv
hpg.o
opphl.l LineG
opphl.d
opphl.g TarskiG
oppcom.a
oppcom.b
oppcom.o
Assertion
Ref Expression
oppne3
Distinct variable groups:   ,,   ,,   ,,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)   (,)   (,)

Proof of Theorem oppne3
StepHypRef Expression
1 hpg.p . . . . . 6
2 eqid 2471 . . . . . 6
3 hpg.i . . . . . 6 Itv
4 opphl.g . . . . . . 7 TarskiG
54ad3antrrr 744 . . . . . 6 TarskiG
6 oppcom.a . . . . . . 7
76ad3antrrr 744 . . . . . 6
8 opphl.l . . . . . . 7 LineG
9 opphl.d . . . . . . . 8
109ad3antrrr 744 . . . . . . 7
11 simplr 770 . . . . . . 7
121, 8, 3, 5, 10, 11tglnpt 24673 . . . . . 6
13 simpr 468 . . . . . . 7
14 simpllr 777 . . . . . . . 8
1514oveq2d 6324 . . . . . . 7
1613, 15eleqtrrd 2552 . . . . . 6
171, 2, 3, 5, 7, 12, 16axtgbtwnid 24593 . . . . 5
1817, 11eqeltrd 2549 . . . 4
19 oppcom.o . . . . . . 7
20 hpg.d . . . . . . . 8
21 hpg.o . . . . . . . 8
22 oppcom.b . . . . . . . 8
231, 20, 3, 21, 6, 22islnopp 24860 . . . . . . 7
2419, 23mpbid 215 . . . . . 6
2524simprd 470 . . . . 5
2625adantr 472 . . . 4
2718, 26r19.29a 2918 . . 3
281, 20, 3, 21, 8, 9, 4, 6, 22, 19oppne1 24862 . . . 4