![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr3i | GIF version |
Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr3i.1 | ⊢ A = B |
3eqtr3i.2 | ⊢ A = 𝐶 |
3eqtr3i.3 | ⊢ B = 𝐷 |
Ref | Expression |
---|---|
3eqtr3i | ⊢ 𝐶 = 𝐷 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3i.1 | . . 3 ⊢ A = B | |
2 | 3eqtr3i.2 | . . 3 ⊢ A = 𝐶 | |
3 | 1, 2 | eqtr3i 2059 | . 2 ⊢ B = 𝐶 |
4 | 3eqtr3i.3 | . 2 ⊢ B = 𝐷 | |
5 | 3, 4 | eqtr3i 2059 | 1 ⊢ 𝐶 = 𝐷 |
Colors of variables: wff set class |
Syntax hints: = wceq 1242 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: csbvarg 2871 un12 3095 in12 3142 indif1 3176 difundir 3184 difindir 3186 dif32 3194 resmpt3 4600 xp0 4686 fvsnun1 5303 caov12 5631 caov13 5633 rec1nq 6379 halfnqq 6393 negsubdii 7092 halfpm6th 7922 i4 9008 imi 9128 |
Copyright terms: Public domain | W3C validator |