![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > oveq1i | Unicode version |
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Ref | Expression |
---|---|
oveq1i.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
oveq1i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | oveq1 5673 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
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-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-rex 2366 df-v 2622 df-un 3004 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-br 3852 df-iota 4993 df-fv 5036 df-ov 5669 |
This theorem is referenced by: caov12 5847 map1 6583 halfnqq 7023 prarloclem5 7113 m1m1sr 7361 caucvgsrlemfv 7390 caucvgsr 7401 pitonnlem1 7436 axi2m1 7464 axcnre 7470 axcaucvg 7489 mvrraddi 7753 mvlladdi 7754 negsubdi 7792 mul02 7919 mulneg1 7927 mulreim 8135 recextlem1 8174 recdivap 8239 2p2e4 8597 2times 8598 3p2e5 8611 3p3e6 8612 4p2e6 8613 4p3e7 8614 4p4e8 8615 5p2e7 8616 5p3e8 8617 5p4e9 8618 6p2e8 8619 6p3e9 8620 7p2e9 8621 1mhlfehlf 8688 8th4div3 8689 halfpm6th 8690 nneoor 8902 9p1e10 8933 dfdec10 8934 num0h 8942 numsuc 8944 dec10p 8973 numma 8974 nummac 8975 numma2c 8976 numadd 8977 numaddc 8978 nummul2c 8980 decaddci 8991 decsubi 8993 decmul1 8994 5p5e10 9001 6p4e10 9002 7p3e10 9005 8p2e10 9010 decbin0 9070 decbin2 9071 elfzp1b 9565 elfzm1b 9566 fz01or 9579 fz1ssfz0 9585 qbtwnrelemcalc 9721 fldiv4p1lem1div2 9766 1tonninf 9900 mulexpzap 10049 expaddzap 10053 sq4e2t8 10106 cu2 10107 i3 10110 iexpcyc 10113 binom2i 10117 binom3 10125 3dec 10177 faclbnd 10203 bcm1k 10222 bcp1nk 10224 bcpasc 10228 hashp1i 10272 hashxp 10288 imre 10339 crim 10346 remullem 10359 resqrexlemfp1 10496 resqrexlemover 10497 resqrexlemcalc1 10501 resqrexlemnm 10505 absexpzap 10567 absimle 10571 amgm2 10605 maxabslemlub 10694 fsumconst 10902 modfsummod 10906 binomlem 10931 binom11 10934 arisum 10946 arisum2 10947 georeclim 10961 geo2sum 10962 mertenslemi1 10983 mertenslem2 10984 mertensabs 10985 efzval 11027 resinval 11060 recosval 11061 efi4p 11062 tan0 11076 efival 11077 cosadd 11082 cos2tsin 11096 ef01bndlem 11101 cos1bnd 11104 cos2bnd 11105 absefib 11114 efieq1re 11115 demoivreALT 11117 eirraplem 11118 3dvdsdec 11197 3dvds2dec 11198 odd2np1 11205 nn0o1gt2 11237 nn0o 11239 flodddiv4 11266 algrp1 11360 3lcm2e6woprm 11400 nn0gcdsq 11510 phiprmpw 11530 ex-fl 11918 ex-exp 11920 ex-bc 11922 qdencn 12181 |
Copyright terms: Public domain | W3C validator |