![]() |
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.) (Proof shortened by Wolf Lammen, 24-Oct-2024.) |
Ref | Expression |
---|---|
eqtr2 | ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2737 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | 1 | biimpa 478 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 |
This theorem is referenced by: eqvincg 3599 reusv3i 5360 moop2 5460 relopabi 5779 relop 5807 f0rn0 6728 fliftfun 7258 soseq 8092 addlsub 11576 wrd2ind 14617 fsum2dlem 15660 fprodser 15837 0dvds 16164 cncongr1 16548 4sqlem12 16833 cshwshashlem1 16973 catideu 17560 pj1eu 19483 lspsneu 20600 1marepvmarrepid 21940 mdetunilem6 21982 qtopeu 23083 qtophmeo 23184 dscmet 23944 isosctrlem2 26185 ppiub 26568 sltsolem1 27039 nolt02o 27059 nogt01o 27060 axcgrtr 27906 axeuclid 27954 axcontlem2 27956 uhgr2edg 28198 usgredgreu 28208 uspgredg2vtxeu 28210 wlkon2n0 28656 spthonepeq 28742 usgr2wlkneq 28746 2pthon3v 28930 umgr2adedgspth 28935 clwwlknondisj 29097 frgr2wwlkeqm 29317 2wspmdisj 29323 ajmoi 29842 chocunii 30285 3oalem2 30647 adjmo 30816 cdjreui 31416 eqtrb 31445 probun 33076 bnj551 33411 satfv0fun 34022 satffunlem 34052 satffunlem1lem1 34053 satffunlem2lem1 34055 btwnswapid 34648 bj-snsetex 35480 bj-bary1lem1 35828 poimirlem4 36128 exidu1 36361 rngoideu 36408 mapdpglem31 40212 remul01 40919 frege55b 42257 frege55c 42278 cncfiooicclem1 44220 euoreqb 45427 aacllem 47334 |
Copyright terms: Public domain | W3C validator |