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 2614 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | 1 | biimpar 501 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 |
This theorem is referenced by: eqtr2 2630 eqtr3 2631 sylan9eq 2664 eqvinc 3300 uneqdifeq 4009 uneqdifeqOLD 4010 preqsnOLD 4332 propeqop 4895 relresfld 5579 unixpid 5587 eqer 7664 eqerOLD 7665 xpider 7705 undifixp 7830 wemaplem2 8335 infeq5 8417 ficard 9266 winalim2 9397 addlsub 10326 pospo 16796 istos 16858 symg2bas 17641 dmatmul 20122 usgra2adedgspthlem2 26140 usgra2wlkspthlem1 26147 eqvincg 28698 bnj545 30219 bnj934 30259 bnj953 30263 poseq 30994 soseq 30995 ordcmp 31616 bj-bary1lem1 32338 poimirlem26 32605 heicant 32614 ismblfin 32620 volsupnfl 32624 itg2addnclem2 32632 itg2addnc 32634 rngodm1dm2 32901 rngoidmlem 32905 rngo1cl 32908 rngoueqz 32909 zerdivemp1x 32916 dvheveccl 35419 rp-isfinite5 36882 clcnvlem 36949 relexpxpmin 37028 gneispace 37452 uhgr2edg 40435 |
Copyright terms: Public domain | W3C validator |