| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > eqtr2i | GIF version | ||
| Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.) |
| Ref | Expression |
|---|---|
| eqtr2i.1 | ⊢ 𝐴 = 𝐵 |
| eqtr2i.2 | ⊢ 𝐵 = 𝐶 |
| Ref | Expression |
|---|---|
| eqtr2i | ⊢ 𝐶 = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqtr2i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
| 2 | eqtr2i.2 | . . 3 ⊢ 𝐵 = 𝐶 | |
| 3 | 1, 2 | eqtri 2225 | . 2 ⊢ 𝐴 = 𝐶 |
| 4 | 3 | eqcomi 2208 | 1 ⊢ 𝐶 = 𝐴 |
| Colors of variables: wff set class |
| Syntax hints: = wceq 1372 |
| 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 1469 ax-gen 1471 ax-4 1532 ax-17 1548 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-cleq 2197 |
| This theorem is referenced by: 3eqtrri 2230 3eqtr2ri 2232 symdif1 3437 dfif3 3583 dfsn2 3646 prprc1 3740 ruv 4596 xpindi 4811 xpindir 4812 dmcnvcnv 4900 rncnvcnv 4901 imainrect 5125 dfrn4 5140 fcoi1 5450 foimacnv 5534 fsnunfv 5775 dfoprab3 6267 fiintim 7010 sbthlemi8 7048 pitonnlem1 7940 ixi 8638 recexaplem2 8707 zeo 9460 num0h 9497 dec10p 9528 fseq1p1m1 10198 fsumrelem 11701 ef0lem 11890 ef01bndlem 11986 3lcm2e6woprm 12327 strsl0 12800 0g0 13126 tgioo 14944 tgqioo 14945 dveflem 15116 sincos4thpi 15230 coskpi 15238 |
| Copyright terms: Public domain | W3C validator |