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

Theorem axtgbtwnid 24377
 Description: Identity of Betweenness. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p
axtrkg.d
axtrkg.i Itv
axtrkg.g TarskiG
axtgbtwnid.1
axtgbtwnid.2
axtgbtwnid.3
Assertion
Ref Expression
axtgbtwnid

Proof of Theorem axtgbtwnid
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 24364 . . . . 5 TarskiG TarskiGC TarskiGB TarskiGCB Itv LineG
2 inss1 3688 . . . . . 6 TarskiGC TarskiGB TarskiGCB Itv LineG TarskiGC TarskiGB
3 inss2 3689 . . . . . 6 TarskiGC TarskiGB TarskiGB
42, 3sstri 3479 . . . . 5 TarskiGC TarskiGB TarskiGCB Itv LineG TarskiGB
51, 4eqsstri 3500 . . . 4 TarskiG TarskiGB
6 axtrkg.g . . . 4 TarskiG
75, 6sseldi 3468 . . 3 TarskiGB
8 axtrkg.p . . . . . 6
9 axtrkg.d . . . . . 6
10 axtrkg.i . . . . . 6 Itv
118, 9, 10istrkgb 24366 . . . . 5 TarskiGB
1211simprbi 465 . . . 4 TarskiGB
1312simp1d 1017 . . 3 TarskiGB
147, 13syl 17 . 2
15 axtgbtwnid.3 . 2
16 axtgbtwnid.1 . . 3
17 axtgbtwnid.2 . . 3
18 id 23 . . . . . . 7
1918, 18oveq12d 6323 . . . . . 6
2019eleq2d 2499 . . . . 5
21 eqeq1 2433 . . . . 5
2220, 21imbi12d 321 . . . 4
23 eleq1 2501 . . . . 5
24 eqeq2 2444 . . . . 5
2523, 24imbi12d 321 . . . 4
2622, 25rspc2v 3197 . . 3
2716, 17, 26syl2anc 665 . 2
2814, 15, 27mp2d 46 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3o 981   w3a 982   wceq 1437   wcel 1870  cab 2414  wral 2782  wrex 2783  crab 2786  cvv 3087  wsbc 3305   cdif 3439   cin 3441  cpw 3985  csn 4002  cfv 5601  (class class class)co 6305   cmpt2 6307  cbs 15084  cds 15161  TarskiGcstrkg 24341  TarskiGCcstrkgc 24342  TarskiGBcstrkgb 24343  TarskiGCBcstrkgcb 24344  Itvcitv 24347  LineGclng 24348 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-trkgb 24360  df-trkg 24364 This theorem is referenced by:  tgbtwncom  24395  tgbtwnne  24397  tgbtwnswapid  24399  tgbtwnintr  24400  tgifscgr  24416  tgidinside  24476  tgbtwnconn1lem3  24479  coltr3  24553  mirinv  24571  miriso  24574  krippenlem  24592  midexlem  24594  colperpexlem3  24631  oppne3  24642  oppnid  24645  opphllem1  24646  midid  24679  lmiisolem  24694  f1otrg  24747
 Copyright terms: Public domain W3C validator