![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqtr | Structured version Visualization version GIF version |
Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.) |
Ref | Expression |
---|---|
eqtr | ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2803 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | 1 | biimpar 470 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-ex 1876 df-cleq 2792 |
This theorem is referenced by: eqtr2 2819 eqtr3 2820 sylan9eq 2853 eqvincg 3518 disjeq0 4218 uneqdifeq 4251 propeqop 5163 relresfld 5881 unixpid 5889 eqer 8017 xpider 8056 undifixp 8184 wemaplem2 8694 infeq5 8784 ficard 9675 winalim2 9806 addlsub 10739 pospo 17288 istos 17350 symg2bas 18130 dmatmul 20629 uhgr2edg 26441 clwlkclwwlkf1lem3 27302 clwlkclwwlkf1lem3OLD 27303 bnj545 31482 bnj934 31522 bnj953 31526 poseq 32266 soseq 32267 ordcmp 32954 bj-snmoore 33561 bj-bary1lem1 33660 poimirlem26 33924 heicant 33933 ismblfin 33939 volsupnfl 33943 itg2addnclem2 33950 itg2addnc 33952 rngodm1dm2 34218 rngoidmlem 34222 rngo1cl 34225 rngoueqz 34226 zerdivemp1x 34233 dvheveccl 37133 rp-isfinite5 38646 clcnvlem 38713 relexpxpmin 38792 gneispace 39214 |
Copyright terms: Public domain | W3C validator |