![]() |
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 2117 |
. 2
![]() ![]() ![]() ![]() |
3 | eqtr3i.2 |
. 2
![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtri 2133 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-4 1468 ax-17 1487 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-cleq 2106 |
This theorem is referenced by: 3eqtr3i 2141 3eqtr3ri 2142 unundi 3201 unundir 3202 inindi 3257 inindir 3258 difun1 3300 difabs 3304 notab 3310 dfrab2 3315 dif0 3397 difdifdirss 3411 tpidm13 3587 intmin2 3761 univ 4355 iunxpconst 4557 dmres 4796 opabresid 4828 rnresi 4852 cnvcnv 4947 rnresv 4954 cnvsn0 4963 cnvsn 4977 resdmres 4986 coi2 5011 coires1 5012 dfdm2 5029 isarep2 5166 ssimaex 5434 fnreseql 5482 fmptpr 5564 idref 5610 mpompt 5815 caov31 5912 xpexgALT 5983 cnvoprab 6083 frec0g 6246 unfiin 6765 xpfi 6769 endjusym 6931 halfnqq 7160 caucvgprlemm 7418 caucvgprprlemmu 7445 caucvgsr 7538 mvlladdi 7897 8th4div3 8837 nneoor 9051 nummac 9124 numadd 9126 numaddc 9127 nummul1c 9128 decbin0 9219 infrenegsupex 9285 iseqvalcbv 10117 m1expcl2 10202 facnn 10360 fac0 10361 4bc3eq4 10406 fihasheq0 10427 resqrexlemcalc1 10672 sqrt1 10704 sqrt4 10705 sqrt9 10706 infxrnegsupex 10918 isumss2 11048 geo2sum2 11170 geoihalfsum 11177 sin0 11281 efival 11284 ef01bndlem 11308 cos2bnd 11312 sin4lt0 11318 flodddiv4 11473 2prm 11648 znnen 11750 ennnfonelemhf1o 11765 setsslid 11846 metreslem 12363 retopbas 12506 |
Copyright terms: Public domain | W3C validator |