![]() |
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 2799 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | 1 | biimpar 478 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-cleq 2788 |
This theorem is referenced by: eqtr2 2817 eqtr3 2818 sylan9eq 2851 eqvincg 3580 disjeq0 4319 uneqdifeq 4352 propeqop 5288 relresfld 6002 unixpid 6010 eqer 8174 xpider 8218 undifixp 8346 wemaplem2 8857 infeq5 8946 ficard 9833 winalim2 9964 addlsub 10904 pospo 17412 istos 17474 symg2bas 18257 dmatmul 20790 uhgr2edg 26673 clwlkclwwlkf1lem3 27471 eqtrb 29930 bnj545 31783 bnj934 31823 bnj953 31827 poseq 32705 soseq 32706 ordcmp 33405 bj-snmoore 34024 bj-bary1lem1 34148 poimirlem26 34468 heicant 34477 ismblfin 34483 volsupnfl 34487 itg2addnclem2 34494 itg2addnc 34496 rngodm1dm2 34761 rngoidmlem 34765 rngo1cl 34768 rngoueqz 34769 zerdivemp1x 34776 dvheveccl 37798 rp-isfinite5 39387 clcnvlem 39487 relexpxpmin 39566 gneispace 39988 |
Copyright terms: Public domain | W3C validator |