Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5eqr | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5eqr.1 | |
syl5eqr.2 |
Ref | Expression |
---|---|
syl5eqr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5eqr.1 | . . 3 | |
2 | 1 | eqcomi 2121 | . 2 |
3 | syl5eqr.2 | . 2 | |
4 | 2, 3 | syl5eq 2162 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: 3eqtr3g 2173 csbeq1a 2983 ssdifeq0 3415 pofun 4204 opabbi2dv 4658 funimaexg 5177 fresin 5271 f1imacnv 5352 foimacnv 5353 fsn2 5562 fmptpr 5580 funiunfvdm 5632 funiunfvdmf 5633 fcof1o 5658 f1opw2 5944 fnexALT 5979 eqerlem 6428 pmresg 6538 mapsn 6552 fopwdom 6698 mapen 6708 fiintim 6785 xpfi 6786 sbthlemi8 6820 sbthlemi9 6821 ctssdccl 6964 exmidfodomrlemim 7025 mul02 8117 recdivap 8446 fzpreddisj 9819 fzshftral 9856 qbtwnrelemcalc 10001 frec2uzrdg 10150 frecuzrdgrcl 10151 frecuzrdgsuc 10155 frecuzrdgrclt 10156 frecuzrdgg 10157 binom3 10377 bcn2 10478 hashfz1 10497 hashunlem 10518 hashfacen 10547 cnrecnv 10650 resqrexlemnm 10758 amgm2 10858 2zsupmax 10965 xrmaxltsup 10995 xrmaxadd 10998 xrbdtri 11013 fisumss 11129 fsumcnv 11174 telfsumo 11203 fsumiun 11214 arisum2 11236 ege2le3 11304 efgt1p 11329 cos01bnd 11392 dfgcd3 11625 eucalgval 11662 sqrt2irrlem 11766 setsslid 11936 baspartn 12144 txdis1cn 12374 cnmpt21 12387 cnmpt22 12390 hmeores 12411 metreslem 12476 remetdval 12635 dvfvalap 12746 nninfsellemqall 13138 |
Copyright terms: Public domain | W3C validator |