![]() |
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 2764 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | 1 | biimpar 503 | 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: eqtr2 2780 eqtr3 2781 sylan9eq 2814 eqvincg 3468 disjeq0 4166 uneqdifeq 4201 uneqdifeqOLD 4202 preqsnOLDOLD 4542 propeqop 5118 relresfld 5823 unixpid 5831 eqer 7948 xpider 7987 undifixp 8112 wemaplem2 8619 infeq5 8709 ficard 9599 winalim2 9730 addlsub 10659 pospo 17194 istos 17256 symg2bas 18038 dmatmul 20525 uhgr2edg 26320 clwlkclwwlkf1lem3 27150 bnj545 31293 bnj934 31333 bnj953 31337 poseq 32080 soseq 32081 ordcmp 32773 bj-snmoore 33392 bj-bary1lem1 33490 poimirlem26 33766 heicant 33775 ismblfin 33781 volsupnfl 33785 itg2addnclem2 33793 itg2addnc 33795 rngodm1dm2 34062 rngoidmlem 34066 rngo1cl 34069 rngoueqz 34070 zerdivemp1x 34077 dvheveccl 36921 rp-isfinite5 38383 clcnvlem 38450 relexpxpmin 38529 gneispace 38952 |
Copyright terms: Public domain | W3C validator |