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 2822 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | 1 | biimpar 478 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 |
This theorem is referenced by: eqtr2 2839 eqtr3 2840 sylan9eq 2873 eqvincg 3638 disjeq0 4401 uneqdifeq 4434 propeqop 5388 relresfld 6120 unixpid 6128 eqer 8313 xpider 8357 undifixp 8486 wemaplem2 8999 infeq5 9088 ficard 9975 winalim2 10106 addlsub 11044 pospo 17571 istos 17633 symg2bas 18455 dmatmul 21034 uhgr2edg 26917 clwlkclwwlkf1lem3 27711 eqtrb 30165 bnj545 32066 bnj934 32106 bnj953 32110 poseq 32992 soseq 32993 ordcmp 33692 bj-snmoore 34299 bj-isclm 34460 bj-bary1lem1 34480 poimirlem26 34799 heicant 34808 ismblfin 34814 volsupnfl 34818 itg2addnclem2 34825 itg2addnc 34827 rngodm1dm2 35091 rngoidmlem 35095 rngo1cl 35098 rngoueqz 35099 zerdivemp1x 35106 dvheveccl 38128 rp-isfinite5 39761 clcnvlem 39861 relexpxpmin 39940 gneispace 40362 |
Copyright terms: Public domain | W3C validator |