Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqtr3 | GIF version |
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) |
Ref | Expression |
---|---|
eqtr3 | ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2166 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵) | |
2 | eqtr 2182 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵) | |
3 | 1, 2 | sylan2b 285 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1342 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: eueq 2892 euind 2908 reuind 2926 preqsn 3749 eusv1 4424 funopg 5216 funinsn 5231 foco 5414 mpofun 5935 enq0tr 7366 lteupri 7549 elrealeu 7761 rereceu 7821 receuap 8557 xrltso 9723 xrlttri3 9724 iseqf1olemab 10414 fsumparts 11397 odd2np1 11795 exmidsbthrlem 13742 |
Copyright terms: Public domain | W3C validator |