![]() |
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 2767 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | eqtr 2779 | . 2 ⊢ ((𝐵 = 𝐴 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) | |
3 | 1, 2 | sylanb 490 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 |
This theorem is referenced by: eqvincg 3468 reusv3i 5024 moop2 5114 relopabi 5401 relop 5428 restidsingOLD 5617 f0rn0 6251 fliftfun 6725 addlsub 10639 wrd2ind 13677 fsum2dlem 14700 fprodser 14878 0dvds 15204 cncongr1 15583 4sqlem12 15862 cshwshashlem1 16004 catideu 16537 pj1eu 18309 lspsneu 19325 1marepvmarrepid 20583 mdetunilem6 20625 qtopeu 21721 qtophmeo 21822 dscmet 22578 isosctrlem2 24748 ppiub 25128 axcgrtr 25994 axeuclid 26042 axcontlem2 26044 uhgr2edg 26299 usgredgreu 26309 uspgredg2vtxeu 26311 wlkon2n0 26772 spthonepeq 26858 usgr2wlkneq 26862 2pthon3v 27063 umgr2adedgspth 27068 clwwlknondisj 27260 clwwlknondisjOLD 27264 frgr2wwlkeqm 27485 2wspmdisj 27491 ajmoi 28023 chocunii 28469 3oalem2 28831 adjmo 29000 cdjreui 29600 probun 30790 bnj551 31119 soseq 32060 sltsolem1 32132 nolt02o 32151 btwnswapid 32430 bj-snsetex 33257 bj-bary1lem1 33472 poimirlem4 33726 exidu1 33968 rngoideu 34015 mapdpglem31 37494 frege55b 38693 frege55c 38714 cncfiooicclem1 40609 aacllem 43060 |
Copyright terms: Public domain | W3C validator |