![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr2i | Unicode 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 2161 |
. 2
![]() ![]() ![]() ![]() |
4 | 3 | eqcomi 2144 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
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: 3eqtrri 2166 3eqtr2ri 2168 symdif1 3346 dfif3 3492 dfsn2 3546 prprc1 3639 ruv 4473 xpindi 4682 xpindir 4683 dmcnvcnv 4771 rncnvcnv 4772 imainrect 4992 dfrn4 5007 fcoi1 5311 foimacnv 5393 fsnunfv 5629 dfoprab3 6097 fiintim 6825 sbthlemi8 6860 pitonnlem1 7677 ixi 8369 recexaplem2 8437 zeo 9180 num0h 9217 dec10p 9248 fseq1p1m1 9905 fsumrelem 11272 ef0lem 11403 ef01bndlem 11499 3lcm2e6woprm 11803 strsl0 12046 tgioo 12754 tgqioo 12755 dveflem 12895 sincos4thpi 12969 coskpi 12977 |
Copyright terms: Public domain | W3C validator |