![]() |
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 2198 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3 | eqcomi 2181 | 1 ⊢ 𝐶 = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1353 |
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 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: 3eqtrri 2203 3eqtr2ri 2205 symdif1 3400 dfif3 3547 dfsn2 3606 prprc1 3700 ruv 4549 xpindi 4762 xpindir 4763 dmcnvcnv 4851 rncnvcnv 4852 imainrect 5074 dfrn4 5089 fcoi1 5396 foimacnv 5479 fsnunfv 5717 dfoprab3 6191 fiintim 6927 sbthlemi8 6962 pitonnlem1 7843 ixi 8538 recexaplem2 8607 zeo 9356 num0h 9393 dec10p 9424 fseq1p1m1 10091 fsumrelem 11474 ef0lem 11663 ef01bndlem 11759 3lcm2e6woprm 12080 strsl0 12505 0g0 12789 tgioo 13977 tgqioo 13978 dveflem 14118 sincos4thpi 14192 coskpi 14200 |
Copyright terms: Public domain | W3C validator |