![]() |
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 2730 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | 1 | biimpa 475 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 |
This theorem is referenced by: eqvincg 3632 reusv3i 5400 moop2 5500 relopabi 5820 relop 5849 f0rn0 6779 fliftfun 7316 soseq 8165 addlsub 11671 wrd2ind 14726 fsum2dlem 15769 fprodser 15946 0dvds 16274 cncongr1 16663 4sqlem12 16953 cshwshashlem1 17093 catideu 17683 pj1eu 19690 lspsneu 21100 1marepvmarrepid 22565 mdetunilem6 22607 qtopeu 23708 qtophmeo 23809 dscmet 24569 isosctrlem2 26844 ppiub 27230 sltsolem1 27702 nolt02o 27722 nogt01o 27723 axcgrtr 28846 axeuclid 28894 axcontlem2 28896 uhgr2edg 29141 usgredgreu 29151 uspgredg2vtxeu 29153 wlkon2n0 29600 spthonepeq 29686 usgr2wlkneq 29690 2pthon3v 29874 umgr2adedgspth 29879 clwwlknondisj 30041 frgr2wwlkeqm 30261 2wspmdisj 30267 ajmoi 30788 chocunii 31231 3oalem2 31593 adjmo 31762 cdjreui 32362 eqtrb 32399 probun 34266 bnj551 34600 satfv0fun 35212 satffunlem 35242 satffunlem1lem1 35243 satffunlem2lem1 35245 r1peuqusdeg1 35484 btwnswapid 35854 bj-snsetex 36683 bj-bary1lem1 37031 poimirlem4 37338 exidu1 37570 rngoideu 37617 mapdpglem31 41415 grpods 41906 remul01 42118 frege55b 43601 frege55c 43622 cncfiooicclem1 45550 euoreqb 46758 isuspgrim0lem 47486 aacllem 48585 |
Copyright terms: Public domain | W3C validator |