| 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 2741 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
| 2 | 1 | biimpa 476 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 |
| This theorem is referenced by: eqvincg 3648 reusv3i 5404 moop2 5507 relopabi 5832 relop 5861 f0rn0 6793 fliftfun 7332 soseq 8184 addlsub 11679 wrd2ind 14761 fsum2dlem 15806 fprodser 15985 0dvds 16314 cncongr1 16704 4sqlem12 16994 cshwshashlem1 17133 catideu 17718 pj1eu 19714 lspsneu 21125 1marepvmarrepid 22581 mdetunilem6 22623 qtopeu 23724 qtophmeo 23825 dscmet 24585 isosctrlem2 26862 ppiub 27248 sltsolem1 27720 nolt02o 27740 nogt01o 27741 axcgrtr 28930 axeuclid 28978 axcontlem2 28980 uhgr2edg 29225 usgredgreu 29235 uspgredg2vtxeu 29237 wlkon2n0 29684 spthonepeq 29772 usgr2wlkneq 29776 2pthon3v 29963 umgr2adedgspth 29968 clwwlknondisj 30130 frgr2wwlkeqm 30350 2wspmdisj 30356 ajmoi 30877 chocunii 31320 3oalem2 31682 adjmo 31851 cdjreui 32451 eqtrb 32493 probun 34421 bnj551 34756 satfv0fun 35376 satffunlem 35406 satffunlem1lem1 35407 satffunlem2lem1 35409 r1peuqusdeg1 35648 btwnswapid 36018 bj-snsetex 36964 bj-bary1lem1 37312 poimirlem4 37631 exidu1 37863 rngoideu 37910 mapdpglem31 41705 grpods 42195 remul01 42437 frege55b 43910 frege55c 43931 cncfiooicclem1 45908 euoreqb 47121 isuspgrim0lem 47871 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |