| 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 2254 | . 2 ⊢ 𝐵 = 𝐶 |
| 4 | 3eqtr3i.3 | . 2 ⊢ 𝐵 = 𝐷 | |
| 5 | 3, 4 | eqtr3i 2254 | 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 2213 |
| This theorem depends on definitions: df-bi 117 df-cleq 2224 |
| This theorem is referenced by: csbvarg 3156 un12 3367 in12 3420 indif1 3454 difundir 3462 difindir 3464 dif32 3472 resmpt3 5068 xp0 5163 fvsnun1 5859 caov12 6221 caov13 6223 djuassen 7475 xpdjuen 7476 rec1nq 7658 halfnqq 7673 negsubdii 8507 halfpm6th 9407 decmul1 9719 i4 10950 fac4 11041 imi 11523 resqrexlemover 11633 ef01bndlem 12380 modsubi 13055 gcdmodi 13057 numexpp1 13060 karatsuba 13066 znnen 13082 sn0cld 14931 cospi 15594 sincos4thpi 15634 sincos3rdpi 15637 lgsdir2lem1 15830 lgsdir2lem5 15834 2lgsoddprmlem3d 15912 ex-bc 16426 ex-gcd 16428 |
| Copyright terms: Public domain | W3C validator |