![]() |
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 2767 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵) | |
2 | eqtr 2779 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵) | |
3 | 1, 2 | sylan2b 493 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 |
This theorem is referenced by: neneor 3031 eueq 3519 euind 3534 reuind 3552 disjeq0 4166 ssprsseq 4502 prnebg 4533 prnesn 4538 preqsnOLDOLD 4542 prel12g 4544 3elpr2eq 4587 eusv1 5009 restidsingOLD 5617 xpcan 5728 xpcan2 5729 funopg 6083 foco 6287 funopdmsn 6579 funsndifnop 6580 mpt2fun 6928 wfr3g 7583 oawordeulem 7805 ixpfi2 8431 wemapso2lem 8624 isf32lem2 9388 fpwwe2lem13 9676 1re 10251 receu 10884 xrlttri 12185 injresinjlem 12802 cshwsexa 13790 fsumparts 14757 odd2np1 15287 prmreclem2 15843 divsfval 16429 isprs 17151 psrn 17430 grpinveu 17677 symgextf1 18061 symgfixf1 18077 efgrelexlemb 18383 lspextmo 19278 evlseu 19738 tgcmp 21426 sqf11 25085 dchrisumlem2 25399 axlowdimlem15 26056 axcontlem2 26065 wlksoneq1eq2 26791 spthonepeq 26879 uspgrn2crct 26932 wwlksnextinj 27038 frgrwopreglem5lem 27495 numclwlk1lem2f1 27537 nsnlplig 27665 nsnlpligALT 27666 grpoinveu 27703 5oalem4 28846 rnbra 29296 xreceu 29960 bnj594 31310 bnj953 31337 frr3g 32106 sltsolem1 32153 nocvxminlem 32220 fnsingle 32353 funimage 32362 funtransport 32465 funray 32574 funline 32576 hilbert1.2 32589 lineintmo 32591 bj-bary1 33491 poimirlem13 33753 poimirlem14 33754 poimirlem17 33757 poimirlem27 33767 prtlem11 34673 prter2 34688 cdleme 36368 kelac2lem 38154 frege124d 38573 2ffzoeq 41866 sprsymrelf1lem 42269 |
Copyright terms: Public domain | W3C validator |