| 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 2741 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
| 2 | 1 | biimpar 477 | 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: eqtr2OLD 2762 eqtr3OLD 2764 sylan9eq 2797 eqvincg 3648 disjeq0 4456 uneqdifeq 4493 propeqop 5512 relresfld 6296 unixpid 6304 fvmptdf 7022 poseq 8183 soseq 8184 eqer 8781 xpider 8828 undifixp 8974 wemaplem2 9587 infeq5 9677 ficard 10605 winalim2 10736 addlsub 11679 pospo 18390 istos 18463 symg2bas 19410 dmatmul 22503 uhgr2edg 29225 clwlkclwwlkf1lem3 30025 eqtrb 32493 bnj545 34909 bnj934 34949 bnj953 34953 ordcmp 36448 bj-snmoore 37114 bj-isclm 37292 bj-bary1lem1 37312 poimirlem26 37653 heicant 37662 ismblfin 37668 volsupnfl 37672 itg2addnclem2 37679 itg2addnc 37681 rngodm1dm2 37939 rngoidmlem 37943 rngo1cl 37946 rngoueqz 37947 zerdivemp1x 37954 disjdmqsss 38803 dvheveccl 41114 rp-isfinite5 43530 clcnvlem 43636 relexpxpmin 43730 gneispace 44147 |
| Copyright terms: Public domain | W3C validator |