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 5749 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1316 (class class class)co 5742 |
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-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-3an 949 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-rex 2399 df-v 2662 df-un 3045 df-sn 3503 df-pr 3504 df-op 3506 df-uni 3707 df-br 3900 df-iota 5058 df-fv 5101 df-ov 5745 |
This theorem is referenced by: caov12 5927 map1 6674 halfnqq 7186 prarloclem5 7276 m1m1sr 7537 caucvgsrlemfv 7567 caucvgsr 7578 pitonnlem1 7621 axi2m1 7651 axcnre 7657 axcaucvg 7676 mvrraddi 7947 mvlladdi 7948 negsubdi 7986 mul02 8117 mulneg1 8125 mulreim 8334 recextlem1 8380 recdivap 8446 2p2e4 8815 2times 8816 3p2e5 8829 3p3e6 8830 4p2e6 8831 4p3e7 8832 4p4e8 8833 5p2e7 8834 5p3e8 8835 5p4e9 8836 6p2e8 8837 6p3e9 8838 7p2e9 8839 1mhlfehlf 8906 8th4div3 8907 halfpm6th 8908 nneoor 9121 9p1e10 9152 dfdec10 9153 num0h 9161 numsuc 9163 dec10p 9192 numma 9193 nummac 9194 numma2c 9195 numadd 9196 numaddc 9197 nummul2c 9199 decaddci 9210 decsubi 9212 decmul1 9213 5p5e10 9220 6p4e10 9221 7p3e10 9224 8p2e10 9229 decbin0 9289 decbin2 9290 elfzp1b 9845 elfzm1b 9846 fz01or 9859 fz1ssfz0 9865 qbtwnrelemcalc 10001 fldiv4p1lem1div2 10046 1tonninf 10181 mulexpzap 10301 expaddzap 10305 sq4e2t8 10358 cu2 10359 i3 10362 iexpcyc 10365 binom2i 10369 binom3 10377 3dec 10429 faclbnd 10455 bcm1k 10474 bcp1nk 10476 bcpasc 10480 hashp1i 10524 hashxp 10540 imre 10591 crim 10598 remullem 10611 resqrexlemfp1 10749 resqrexlemover 10750 resqrexlemcalc1 10754 resqrexlemnm 10758 absexpzap 10820 absimle 10824 amgm2 10858 maxabslemlub 10947 fsumconst 11191 modfsummod 11195 binomlem 11220 binom11 11223 arisum 11235 arisum2 11236 georeclim 11250 geo2sum 11251 mertenslemi1 11272 mertenslem2 11273 mertensabs 11274 efzval 11316 resinval 11349 recosval 11350 efi4p 11351 tan0 11365 efival 11366 cosadd 11371 cos2tsin 11385 ef01bndlem 11390 cos1bnd 11393 cos2bnd 11394 absefib 11404 efieq1re 11405 demoivreALT 11407 eirraplem 11410 3dvdsdec 11489 3dvds2dec 11490 odd2np1 11497 nn0o1gt2 11529 nn0o 11531 flodddiv4 11558 algrp1 11654 3lcm2e6woprm 11694 nn0gcdsq 11805 phiprmpw 11825 cnmpt1res 12392 rerestcntop 12646 dvfvalap 12746 dvcnp2cntop 12759 dveflem 12782 sin0pilem1 12789 sinhalfpilem 12799 cospi 12808 eulerid 12810 cos2pi 12812 ef2kpi 12814 sinhalfpip 12828 sinhalfpim 12829 coshalfpip 12830 coshalfpim 12831 sincosq3sgn 12836 sincosq4sgn 12837 cosq23lt0 12841 tangtx 12846 sincos4thpi 12848 sincos6thpi 12850 cosq34lt1 12858 ex-fl 12864 ex-exp 12866 ex-bc 12868 qdencn 13149 isomninnlem 13152 |
Copyright terms: Public domain | W3C validator |