| 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 2255 | . 2 ⊢ 𝐵 = 𝐶 |
| 4 | 3eqtr3i.3 | . 2 ⊢ 𝐵 = 𝐷 | |
| 5 | 3, 4 | eqtr3i 2255 | 1 ⊢ 𝐶 = 𝐷 |
| Colors of variables: wff set class |
| Syntax hints: = wceq 1398 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1496 ax-gen 1498 ax-4 1559 ax-17 1575 ax-ext 2214 |
| This theorem depends on definitions: df-bi 117 df-cleq 2225 |
| This theorem is referenced by: csbvarg 3165 un12 3376 in12 3429 indif1 3463 difundir 3471 difindir 3473 dif32 3481 resmpt3 5078 xp0 5173 fvsnun1 5872 caov12 6234 caov13 6236 djuassen 7515 xpdjuen 7516 rec1nq 7698 halfnqq 7713 negsubdii 8546 halfpm6th 9446 decmul1 9758 i4 10990 fac4 11081 imi 11563 resqrexlemover 11673 ef01bndlem 12420 modsubi 13095 gcdmodi 13097 numexpp1 13100 karatsuba 13106 znnen 13123 sn0cld 14972 cospi 15635 sincos4thpi 15675 sincos3rdpi 15678 lgsdir2lem1 15871 lgsdir2lem5 15875 2lgsoddprmlem3d 15953 ex-bc 16467 ex-gcd 16469 |
| Copyright terms: Public domain | W3C validator |