![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqtr2 | Structured version Visualization version Unicode version |
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
eqtr2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2478 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqtr 2490 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylanb 480 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-cleq 2464 |
This theorem is referenced by: eqvinc 3154 reusv3i 4608 moop2 4696 relop 4990 restidsing 5167 f0rn0 5781 fliftfun 6223 addlsub 10057 wrd2ind 12888 fsum2dlem 13908 fprodser 14080 0dvds 14400 4sqlem12 14979 cshwshashlem1 15144 catideu 15659 pj1eu 17424 lspsneu 18424 1marepvmarrepid 19677 mdetunilem6 19719 qtopeu 20808 qtophmeo 20909 dscmet 21665 isosctrlem2 23827 ppiub 24211 axcgrtr 25024 axeuclid 25072 axcontlem2 25074 usgraedgprv 25182 usgra2edg 25188 usgraedgreu 25194 spthonepeq 25396 wlkdvspthlem 25416 usgra2wlkspthlem1 25426 el2wlkonotot0 25679 2spotdisj 25868 numclwwlkdisj 25887 exidu1 26135 rngoideu 26193 ajmoi 26581 chocunii 27035 3oalem2 27397 adjmo 27566 cdjreui 28166 eqvincg 28189 probun 29325 bnj551 29624 soseq 30563 sltsolem1 30628 btwnswapid 30855 bj-snsetex 31627 bj-bary1lem1 31786 poimirlem4 32008 mapdpglem31 35342 frege55b 36564 frege55c 36585 cncfiooicclem1 37868 uhgr2edg 39453 usgredgreu 39459 uspgredg2vtxeu 39461 spthonepeq-av 39944 usgr2wlkneq 39948 2pthon3v-av 40065 umgr2adedgspth 40070 usgvincvadeu 40225 usgvincvadeuALT 40228 aacllem 41046 |
Copyright terms: Public domain | W3C validator |