Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > oveq12i | Unicode version |
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Ref | Expression |
---|---|
oveq1i.1 | |
oveq12i.2 |
Ref | Expression |
---|---|
oveq12i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1i.1 | . 2 | |
2 | oveq12i.2 | . 2 | |
3 | oveq12 5834 | . 2 | |
4 | 1, 2, 3 | mp2an 423 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1335 (class class class)co 5825 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-rex 2441 df-v 2714 df-un 3106 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3774 df-br 3967 df-iota 5136 df-fv 5179 df-ov 5828 |
This theorem is referenced by: oveq123i 5839 1lt2nq 7327 halfnqq 7331 caucvgprprlemnbj 7614 caucvgprprlemaddq 7629 m1p1sr 7681 m1m1sr 7682 axi2m1 7796 negdii 8160 3t3e9 8991 8th4div3 9053 halfpm6th 9054 numma 9339 decmul10add 9364 4t3lem 9392 9t11e99 9425 halfthird 9438 5recm6rec 9439 fz0to3un2pr 10026 sqdivapi 10506 sq4e2t8 10520 i4 10525 binom2i 10531 facp1 10608 fac2 10609 fac3 10610 fac4 10611 4bc2eq6 10652 cji 10806 fsumadd 11307 fsumsplitf 11309 fsumsplitsnun 11320 0.999... 11422 fprodmul 11492 fprodsplitf 11533 ef01bndlem 11657 cos2bnd 11661 3dvds2dec 11761 flodddiv4 11829 nn0gcdsq 12079 pythagtriplem16 12158 cnmpt2res 12739 txmetcnp 12960 dveflem 13129 efhalfpi 13162 efipi 13164 sin2pi 13166 ef2pi 13168 sincosq3sgn 13191 sincosq4sgn 13192 sinq34lt0t 13194 sincos4thpi 13203 tan4thpi 13204 sincos6thpi 13205 sincos3rdpi 13206 pigt3 13207 ex-exp 13345 ex-fac 13346 ex-bc 13347 |
Copyright terms: Public domain | W3C validator |