![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqtr2 | Structured version Visualization version GIF 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 2779 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | eqtr 2793 | . 2 ⊢ ((𝐵 = 𝐴 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) | |
3 | 1, 2 | sylanb 573 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-9 2057 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2765 |
This theorem is referenced by: eqvincg 3550 reusv3i 5152 moop2 5241 relopabi 5537 relop 5564 f0rn0 6387 fliftfun 6882 addlsub 10849 wrd2ind 13907 wrd2indOLD 13908 fsum2dlem 14975 fprodser 15153 0dvds 15480 cncongr1 15857 4sqlem12 16138 cshwshashlem1 16275 catideu 16794 pj1eu 18570 lspsneu 19607 1marepvmarrepid 20878 mdetunilem6 20920 qtopeu 22018 qtophmeo 22119 dscmet 22875 isosctrlem2 25088 ppiub 25472 axcgrtr 26394 axeuclid 26442 axcontlem2 26444 uhgr2edg 26683 usgredgreu 26693 uspgredg2vtxeu 26695 wlkon2n0 27140 spthonepeq 27231 usgr2wlkneq 27235 2pthon3v 27439 umgr2adedgspth 27444 clwwlknondisj 27629 frgr2wwlkeqm 27855 2wspmdisj 27861 ajmoi 28403 chocunii 28849 3oalem2 29211 adjmo 29380 cdjreui 29980 eqtrb 30010 probun 31280 bnj551 31622 soseq 32557 sltsolem1 32641 nolt02o 32660 btwnswapid 32939 bj-snsetex 33728 bj-bary1lem1 33975 poimirlem4 34285 exidu1 34524 rngoideu 34571 mapdpglem31 38232 frege55b 39551 frege55c 39572 cncfiooicclem1 41552 euoreqb 42660 aacllem 44209 |
Copyright terms: Public domain | W3C validator |