Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqtr3 | Structured version Visualization version GIF version |
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) |
Ref | Expression |
---|---|
eqtr3 | ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2617 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵) | |
2 | eqtr 2629 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵) | |
3 | 1, 2 | sylan2b 491 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 |
This theorem is referenced by: neneor 2881 eueq 3345 euind 3360 reuind 3378 ssprsseq 4297 prnebg 4329 preqsnOLD 4332 eusv1 4786 restidsingOLD 5378 xpcan 5489 xpcan2 5490 funopg 5836 foco 6038 funsndifnop 6321 mpt2fun 6660 wfr3g 7300 oawordeulem 7521 ixpfi2 8147 wemapso2lem 8340 isf32lem2 9059 fpwwe2lem13 9343 1re 9918 receu 10551 xrlttri 11848 injresinjlem 12450 cshwsexa 13421 fsumparts 14379 odd2np1 14903 prmreclem2 15459 divsfval 16030 isprs 16753 psrn 17032 grpinveu 17279 symgextf1 17664 symgfixf1 17680 efgrelexlemb 17986 lspextmo 18877 evlseu 19337 tgcmp 21014 sqf11 24665 dchrisumlem2 24979 axlowdimlem15 25636 axcontlem2 25645 nbgraf1olem1 25970 spthonepeq 26117 usgrcyclnl2 26169 4cycl4dv 26195 wwlkextinj 26258 numclwlk1lem2f1 26621 grpoinveu 26757 5oalem4 27900 rnbra 28350 xreceu 28961 bnj594 30236 bnj953 30263 frr3g 31023 sltsolem1 31067 nocvxminlem 31089 fnsingle 31196 funimage 31205 funtransport 31308 funray 31417 funline 31419 hilbert1.2 31432 lineintmo 31434 bj-bary1 32339 poimirlem13 32592 poimirlem14 32593 poimirlem17 32596 poimirlem27 32606 prtlem11 33169 prter2 33184 cdleme 34866 kelac2lem 36652 frege124d 37072 2ffzoeq 40361 wlksoneq1eq2 40872 spthonepeq-av 40958 uspgrn2crct 41011 wwlksnextinj 41105 av-numclwlk1lem2f1 41524 |
Copyright terms: Public domain | W3C validator |