Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqtr3i | GIF version |
Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.) |
Ref | Expression |
---|---|
eqtr3i.1 | ⊢ 𝐴 = 𝐵 |
eqtr3i.2 | ⊢ 𝐴 = 𝐶 |
Ref | Expression |
---|---|
eqtr3i | ⊢ 𝐵 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr3i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 1 | eqcomi 2121 | . 2 ⊢ 𝐵 = 𝐴 |
3 | eqtr3i.2 | . 2 ⊢ 𝐴 = 𝐶 | |
4 | 2, 3 | eqtri 2138 | 1 ⊢ 𝐵 = 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1316 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: 3eqtr3i 2146 3eqtr3ri 2147 unundi 3207 unundir 3208 inindi 3263 inindir 3264 difun1 3306 difabs 3310 notab 3316 dfrab2 3321 dif0 3403 difdifdirss 3417 tpidm13 3593 intmin2 3767 univ 4367 iunxpconst 4569 dmres 4810 opabresid 4842 rnresi 4866 cnvcnv 4961 rnresv 4968 cnvsn0 4977 cnvsn 4991 resdmres 5000 coi2 5025 coires1 5026 dfdm2 5043 isarep2 5180 ssimaex 5450 fnreseql 5498 fmptpr 5580 idref 5626 mpompt 5831 caov31 5928 xpexgALT 5999 cnvoprab 6099 frec0g 6262 unfiin 6782 xpfi 6786 endjusym 6949 halfnqq 7186 caucvgprlemm 7444 caucvgprprlemmu 7471 caucvgsr 7578 mvlladdi 7948 8th4div3 8907 nneoor 9121 nummac 9194 numadd 9196 numaddc 9197 nummul1c 9198 decbin0 9289 infrenegsupex 9357 iseqvalcbv 10198 m1expcl2 10283 facnn 10441 fac0 10442 4bc3eq4 10487 fihasheq0 10508 resqrexlemcalc1 10754 sqrt1 10786 sqrt4 10787 sqrt9 10788 infxrnegsupex 11000 isumss2 11130 geo2sum2 11252 geoihalfsum 11259 sin0 11363 efival 11366 ef01bndlem 11390 cos2bnd 11394 sin4lt0 11400 flodddiv4 11558 2prm 11735 znnen 11838 ennnfonelemhf1o 11853 setsslid 11936 metreslem 12476 retopbas 12619 sinhalfpilem 12799 sincos6thpi 12850 sincos3rdpi 12851 |
Copyright terms: Public domain | W3C validator |