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 2174 | . 2 |
3 | eqtr3id.2 | . 2 | |
4 | 2, 3 | eqtrid 2215 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1348 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: 3eqtr3g 2226 csbeq1a 3058 ssdifeq0 3497 pofun 4297 opabbi2dv 4760 funimaexg 5282 fresin 5376 f1imacnv 5459 foimacnv 5460 fsn2 5670 fmptpr 5688 funiunfvdm 5742 funiunfvdmf 5743 fcof1o 5768 f1opw2 6055 fnexALT 6090 eqerlem 6544 pmresg 6654 mapsn 6668 fopwdom 6814 mapen 6824 fiintim 6906 xpfi 6907 sbthlemi8 6941 sbthlemi9 6942 ctssdccl 7088 exmidfodomrlemim 7178 mul02 8306 recdivap 8635 fzpreddisj 10027 fzshftral 10064 qbtwnrelemcalc 10212 frec2uzrdg 10365 frecuzrdgrcl 10366 frecuzrdgsuc 10370 frecuzrdgrclt 10371 frecuzrdgg 10372 binom3 10593 bcn2 10698 hashfz1 10717 hashunlem 10739 hashfacen 10771 cnrecnv 10874 resqrexlemnm 10982 amgm2 11082 2zsupmax 11189 xrmaxltsup 11221 xrmaxadd 11224 xrbdtri 11239 fisumss 11355 fsumcnv 11400 telfsumo 11429 fsumiun 11440 arisum2 11462 fprodssdc 11553 fprodsplitdc 11559 fprodsplit 11560 fprodcnv 11588 ege2le3 11634 efgt1p 11659 cos01bnd 11721 suprzubdc 11907 dfgcd3 11965 eucalgval 12008 sqrt2irrlem 12115 pcid 12277 setsslid 12466 baspartn 12842 txdis1cn 13072 cnmpt21 13085 cnmpt22 13088 hmeores 13109 metreslem 13174 remetdval 13333 dvfvalap 13444 binom4 13691 1lgs 13738 lgs1 13739 nninfsellemqall 14048 |
Copyright terms: Public domain | W3C validator |