Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > tgcgrcomlr | Structured version Visualization version Unicode version |
Description: Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
Ref | Expression |
---|---|
tkgeom.p | |
tkgeom.d | |
tkgeom.i | Itv |
tkgeom.g | TarskiG |
tgcgrcomlr.a | |
tgcgrcomlr.b | |
tgcgrcomlr.c | |
tgcgrcomlr.d | |
tgcgrcomlr.6 |
Ref | Expression |
---|---|
tgcgrcomlr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgcgrcomlr.6 | . 2 | |
2 | tkgeom.p | . . 3 | |
3 | tkgeom.d | . . 3 | |
4 | tkgeom.i | . . 3 Itv | |
5 | tkgeom.g | . . 3 TarskiG | |
6 | tgcgrcomlr.a | . . 3 | |
7 | tgcgrcomlr.b | . . 3 | |
8 | 2, 3, 4, 5, 6, 7 | axtgcgrrflx 25361 | . 2 |
9 | tgcgrcomlr.c | . . 3 | |
10 | tgcgrcomlr.d | . . 3 | |
11 | 2, 3, 4, 5, 9, 10 | axtgcgrrflx 25361 | . 2 |
12 | 1, 8, 11 | 3eqtr3d 2664 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 wcel 1990 cfv 5888 (class class class)co 6650 cbs 15857 cds 15950 TarskiGcstrkg 25329 Itvcitv 25335 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-trkgc 25347 df-trkg 25352 |
This theorem is referenced by: tgcgrextend 25380 tgifscgr 25403 tgcgrsub 25404 iscgrglt 25409 trgcgrg 25410 tgcgrxfr 25413 cgr3swap12 25418 cgr3swap23 25419 tgbtwnxfr 25425 lnext 25462 tgbtwnconn1lem1 25467 tgbtwnconn1lem2 25468 tgbtwnconn1lem3 25469 tgbtwnconn1 25470 legov2 25481 legtri3 25485 legbtwn 25489 tgcgrsub2 25490 miriso 25565 mircgrextend 25577 mirtrcgr 25578 miduniq 25580 colmid 25583 symquadlem 25584 krippenlem 25585 midexlem 25587 ragcom 25593 ragflat 25599 ragcgr 25602 footex 25613 colperpexlem1 25622 mideulem2 25626 opphllem 25627 opphllem3 25641 lmiisolem 25688 hypcgrlem1 25691 trgcopy 25696 trgcopyeulem 25697 iscgra1 25702 cgracgr 25710 cgraswap 25712 cgrcgra 25713 cgracom 25714 cgratr 25715 dfcgra2 25721 sacgr 25722 acopy 25724 acopyeu 25725 cgrg3col4 25734 tgsas1 25735 tgsas3 25738 tgasa1 25739 |
Copyright terms: Public domain | W3C validator |