Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqtr3id | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtr3id.1 | |
eqtr3id.2 |
Ref | Expression |
---|---|
eqtr3id |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr3id.1 | . . 3 | |
2 | 1 | eqcomi 2161 | . 2 |
3 | eqtr3id.2 | . 2 | |
4 | 2, 3 | syl5eq 2202 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1335 |
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 1427 ax-gen 1429 ax-4 1490 ax-17 1506 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-cleq 2150 |
This theorem is referenced by: 3eqtr3g 2213 csbeq1a 3040 ssdifeq0 3477 pofun 4275 opabbi2dv 4738 funimaexg 5257 fresin 5351 f1imacnv 5434 foimacnv 5435 fsn2 5644 fmptpr 5662 funiunfvdm 5716 funiunfvdmf 5717 fcof1o 5742 f1opw2 6029 fnexALT 6064 eqerlem 6514 pmresg 6624 mapsn 6638 fopwdom 6784 mapen 6794 fiintim 6876 xpfi 6877 sbthlemi8 6911 sbthlemi9 6912 ctssdccl 7058 exmidfodomrlemim 7139 mul02 8267 recdivap 8596 fzpreddisj 9980 fzshftral 10017 qbtwnrelemcalc 10165 frec2uzrdg 10318 frecuzrdgrcl 10319 frecuzrdgsuc 10323 frecuzrdgrclt 10324 frecuzrdgg 10325 binom3 10545 bcn2 10650 hashfz1 10669 hashunlem 10690 hashfacen 10719 cnrecnv 10822 resqrexlemnm 10930 amgm2 11030 2zsupmax 11137 xrmaxltsup 11167 xrmaxadd 11170 xrbdtri 11185 fisumss 11301 fsumcnv 11346 telfsumo 11375 fsumiun 11386 arisum2 11408 fprodssdc 11499 fprodsplitdc 11505 fprodsplit 11506 fprodcnv 11534 ege2le3 11580 efgt1p 11605 cos01bnd 11667 suprzubdc 11852 dfgcd3 11910 eucalgval 11947 sqrt2irrlem 12052 pcid 12213 setsslid 12336 baspartn 12544 txdis1cn 12774 cnmpt21 12787 cnmpt22 12790 hmeores 12811 metreslem 12876 remetdval 13035 dvfvalap 13146 binom4 13393 nninfsellemqall 13684 |
Copyright terms: Public domain | W3C validator |