![]() |
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 2087 | . 2 ⊢ 𝐵 = 𝐴 |
3 | eqtr3i.2 | . 2 ⊢ 𝐴 = 𝐶 | |
4 | 2, 3 | eqtri 2103 | 1 ⊢ 𝐵 = 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1285 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-4 1441 ax-17 1460 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-cleq 2076 |
This theorem is referenced by: 3eqtr3i 2111 3eqtr3ri 2112 unundi 3144 unundir 3145 inindi 3200 inindir 3201 difun1 3241 difabs 3245 notab 3251 dfrab2 3256 dif0 3331 difdifdirss 3344 tpidm13 3511 intmin2 3683 univ 4254 iunxpconst 4447 dmres 4681 opabresid 4710 rnresi 4733 cnvcnv 4824 rnresv 4831 cnvsn0 4840 cnvsn 4854 resdmres 4863 coi2 4888 coires1 4889 dfdm2 4903 isarep2 5038 ssimaex 5288 fnreseql 5331 fmptpr 5409 idref 5450 mpt2mpt 5649 caov31 5743 xpexgALT 5813 cnvoprab 5908 frec0g 6068 unfiin 6472 xpfi 6474 djuin 6563 halfnqq 6739 caucvgprlemm 6997 caucvgprprlemmu 7024 caucvgsr 7117 mvlladdi 7470 8th4div3 8394 nneoor 8607 nummac 8679 numadd 8681 numaddc 8682 nummul1c 8683 decbin0 8774 infrenegsupex 8840 iseqvalcbv 9608 m1expcl2 9672 facnn 9828 fac0 9829 4bc3eq4 9874 fihasheq0 9895 resqrexlemcalc1 10126 sqrt1 10158 sqrt4 10159 sqrt9 10160 flodddiv4 10566 2prm 10741 znnen 10843 |
Copyright terms: Public domain | W3C validator |