| 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.) (Proof shortened by Wolf Lammen, 24-Oct-2024.) |
| Ref | Expression |
|---|---|
| eqtr3 | ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq2 2749 | . 2 ⊢ (𝐵 = 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶)) | |
| 2 | 1 | biimparc 479 | 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: neneor 3042 moeq 3713 euind 3730 reuind 3759 disjeq0 4456 ssprsseq 4825 mosneq 4842 prnebg 4856 prnesn 4860 prel12g 4864 3elpr2eq 4906 eusv1 5391 xpcan 6196 xpcan2 6197 funopg 6600 funopdmsn 7170 funsndifnop 7171 fvf1pr 7327 resf1extb 7956 wfr3g 8347 oawordeulem 8592 nnasmo 8701 en1eqsn 9308 ixpfi2 9390 frr3g 9796 isf32lem2 10394 fpwwe2lem12 10682 1re 11261 receu 11908 xrlttri 13181 injresinjlem 13826 cshwsexaOLD 14863 fsumparts 15842 odd2np1 16378 prmreclem2 16955 divsfval 17592 isprs 18342 psrn 18620 grpinveu 18992 symgextf1 19439 symgfixf1 19455 efgrelexlemb 19768 lspextmo 21055 evlseu 22107 tgcmp 23409 sqf11 27182 dchrisumlem2 27534 sltsolem1 27720 nocvxminlem 27822 divsmo 28210 axlowdimlem15 28971 axcontlem2 28980 wlksoneq1eq2 29682 spthonepeq 29772 uspgrn2crct 29828 wwlksnextinj 29919 frgrwopreglem5lem 30339 numclwwlk1lem2f1 30376 nsnlplig 30500 nsnlpligALT 30501 grpoinveu 30538 5oalem4 31676 rnbra 32126 xreceu 32904 bnj594 34926 bnj953 34953 fnsingle 35920 funimage 35929 funtransport 36032 funray 36141 funline 36143 hilbert1.2 36156 lineintmo 36158 bj-bary1 37313 poimirlem13 37640 poimirlem14 37641 poimirlem17 37644 poimirlem27 37654 antisymressn 38445 disjdmqscossss 38804 prter2 38882 cdleme 40562 kelac2lem 43076 frege124d 43774 2ffzoeq 47339 sprsymrelf1lem 47478 paireqne 47498 usgrexmpl2trifr 47996 gpg5grlic 48047 mof0ALT 48749 mofsn 48753 f1omo 48792 oppcendc 48906 |
| Copyright terms: Public domain | W3C validator |