![]() |
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 | ⊢ 𝐴 = 𝐵 |
3eqtr3i.2 | ⊢ 𝐴 = 𝐶 |
3eqtr3i.3 | ⊢ 𝐵 = 𝐷 |
Ref | Expression |
---|---|
3eqtr3i | ⊢ 𝐶 = 𝐷 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 3eqtr3i.2 | . . 3 ⊢ 𝐴 = 𝐶 | |
3 | 1, 2 | eqtr3i 2163 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 3eqtr3i.3 | . 2 ⊢ 𝐵 = 𝐷 | |
5 | 3, 4 | eqtr3i 2163 | 1 ⊢ 𝐶 = 𝐷 |
Colors of variables: wff set class |
Syntax hints: = wceq 1332 |
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 1424 ax-gen 1426 ax-4 1488 ax-17 1507 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 |
This theorem is referenced by: csbvarg 3035 un12 3239 in12 3292 indif1 3326 difundir 3334 difindir 3336 dif32 3344 resmpt3 4876 xp0 4966 fvsnun1 5625 caov12 5967 caov13 5969 djuassen 7090 xpdjuen 7091 rec1nq 7227 halfnqq 7242 negsubdii 8071 halfpm6th 8964 decmul1 9269 i4 10426 fac4 10511 imi 10704 resqrexlemover 10814 ef01bndlem 11499 znnen 11947 sn0cld 12345 cospi 12929 sincos4thpi 12969 sincos3rdpi 12972 ex-bc 13112 ex-gcd 13114 |
Copyright terms: Public domain | W3C validator |