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 2139 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵) | |
2 | eqtr 2155 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵) | |
3 | 1, 2 | sylan2b 285 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1331 |
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 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-cleq 2130 |
This theorem is referenced by: eueq 2850 euind 2866 reuind 2884 preqsn 3697 eusv1 4368 funopg 5152 funinsn 5167 foco 5350 mpofun 5866 enq0tr 7235 lteupri 7418 elrealeu 7630 rereceu 7690 receuap 8423 xrltso 9575 xrlttri3 9576 iseqf1olemab 10255 fsumparts 11232 odd2np1 11559 exmidsbthrlem 13206 |
Copyright terms: Public domain | W3C validator |