![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > oveq12 | Unicode version |
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
Ref | Expression |
---|---|
oveq12 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 5884 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | oveq2 5885 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan9eq 2230 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rex 2461 df-v 2741 df-un 3135 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-br 4006 df-iota 5180 df-fv 5226 df-ov 5880 |
This theorem is referenced by: oveq12i 5889 oveq12d 5895 oveqan12d 5896 ecopoveq 6632 ecopovtrn 6634 ecopovtrng 6637 th3qlem1 6639 th3qlem2 6640 mulcmpblnq 7369 addpipqqs 7371 ordpipqqs 7375 enq0breq 7437 mulcmpblnq0 7445 nqpnq0nq 7454 nqnq0a 7455 nqnq0m 7456 nq0m0r 7457 nq0a0 7458 distrlem5prl 7587 distrlem5pru 7588 addcmpblnr 7740 ltsrprg 7748 mulgt0sr 7779 add20 8433 cru 8561 qaddcl 9637 qmulcl 9639 xaddval 9847 xnn0xadd0 9869 fzopth 10063 modqval 10326 seqvalcd 10461 seqovcd 10465 1exp 10551 m1expeven 10569 nn0opthd 10704 faclbnd 10723 faclbnd3 10725 bcn0 10737 reval 10860 absval 11012 clim 11291 fsumparts 11480 dvds2add 11834 dvds2sub 11835 opoe 11902 omoe 11903 opeo 11904 omeo 11905 gcddvds 11966 gcdcl 11969 gcdeq0 11980 gcdneg 11985 gcdaddm 11987 gcdabs 11991 gcddiv 12022 eucalgval2 12055 lcmabs 12078 rpmul 12100 divgcdcoprmex 12104 prmexpb 12153 rpexp 12155 nn0gcdsq 12202 pcqmul 12305 mul4sq 12394 f1ocpbl 12737 plusfvalg 12787 0subm 12876 ringadd2 13215 aprval 13377 scafvalg 13402 rmodislmodlem 13445 rmodislmod 13446 lss1d 13475 cnmpt2t 13878 cnmpt22f 13880 hmeofvalg 13888 bdmetval 14085 mul2sq 14548 |
Copyright terms: Public domain | W3C validator |