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 2629 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵) | |
2 | eqtr 2641 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵) | |
3 | 1, 2 | sylan2b 492 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 |
This theorem is referenced by: neneor 2893 eueq 3378 euind 3393 reuind 3411 ssprsseq 4357 prnebg 4389 preqsnOLD 4394 3elpr2eq 4435 eusv1 4860 restidsingOLD 5459 xpcan 5570 xpcan2 5571 funopg 5922 foco 6125 funopdmsn 6415 funsndifnop 6416 mpt2fun 6762 wfr3g 7413 oawordeulem 7634 ixpfi2 8264 wemapso2lem 8457 isf32lem2 9176 fpwwe2lem13 9464 1re 10039 receu 10672 xrlttri 11972 injresinjlem 12588 cshwsexa 13570 fsumparts 14538 odd2np1 15065 prmreclem2 15621 divsfval 16207 isprs 16930 psrn 17209 grpinveu 17456 symgextf1 17841 symgfixf1 17857 efgrelexlemb 18163 lspextmo 19056 evlseu 19516 tgcmp 21204 sqf11 24865 dchrisumlem2 25179 axlowdimlem15 25836 axcontlem2 25845 wlksoneq1eq2 26560 spthonepeq 26648 uspgrn2crct 26700 wwlksnextinj 26794 frgrwopreglem5lem 27184 numclwlk1lem2f1 27227 nsnlplig 27333 nsnlpligALT 27334 grpoinveu 27373 5oalem4 28516 rnbra 28966 xreceu 29630 bnj594 30982 bnj953 31009 frr3g 31779 sltsolem1 31826 nocvxminlem 31893 fnsingle 32026 funimage 32035 funtransport 32138 funray 32247 funline 32249 hilbert1.2 32262 lineintmo 32264 bj-bary1 33162 poimirlem13 33422 poimirlem14 33423 poimirlem17 33426 poimirlem27 33436 prtlem11 34151 prter2 34166 cdleme 35848 kelac2lem 37634 frege124d 38053 2ffzoeq 41338 sprsymrelf1lem 41741 |
Copyright terms: Public domain | W3C validator |