![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr3i | Unicode 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 2193 |
. 2
![]() ![]() ![]() ![]() |
3 | eqtr3i.2 |
. 2
![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtri 2210 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: 3eqtr3i 2218 3eqtr3ri 2219 unundi 3311 unundir 3312 inindi 3367 inindir 3368 difun1 3410 difabs 3414 notab 3420 dfrab2 3425 dif0 3508 difdifdirss 3522 tpidm13 3707 intmin2 3885 univ 4491 iunxpconst 4701 dmres 4943 opabresid 4975 rnresi 5000 cnvcnv 5096 rnresv 5103 cnvsn0 5112 cnvsn 5126 resdmres 5135 coi2 5160 coires1 5161 dfdm2 5178 isarep2 5319 ssimaex 5594 fnreseql 5643 fmptpr 5725 idref 5774 mpompt 5984 caov31 6082 xpexgALT 6153 cnvoprab 6254 frec0g 6417 unfiin 6949 xpfi 6953 endjusym 7120 halfnqq 7434 caucvgprlemm 7692 caucvgprprlemmu 7719 caucvgsr 7826 mvlladdi 8200 8th4div3 9163 nneoor 9380 nummac 9453 numadd 9455 numaddc 9456 nummul1c 9457 decbin0 9548 infrenegsupex 9619 iseqvalcbv 10483 m1expcl2 10568 facnn 10734 fac0 10735 4bc3eq4 10780 fihasheq0 10800 resqrexlemcalc1 11050 sqrt1 11082 sqrt4 11083 sqrt9 11084 infxrnegsupex 11298 isumss2 11428 geo2sum2 11550 geoihalfsum 11557 sin0 11764 efival 11767 ef01bndlem 11791 cos2bnd 11795 sin4lt0 11801 flodddiv4 11966 2prm 12154 znnen 12444 ennnfonelemhf1o 12459 setsslid 12558 ressressg 12580 metreslem 14317 retopbas 14460 sinhalfpilem 14649 sincos6thpi 14700 sincos3rdpi 14701 lgsdir2lem3 14868 lgseisenlem1 14887 lgseisenlem2 14888 2lgsoddprmlem2 14891 |
Copyright terms: Public domain | W3C validator |