![]() |
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 5733 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | oveq2 5734 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan9eq 2165 |
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 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-3an 945 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-rex 2394 df-v 2657 df-un 3039 df-sn 3497 df-pr 3498 df-op 3500 df-uni 3701 df-br 3894 df-iota 5044 df-fv 5087 df-ov 5729 |
This theorem is referenced by: oveq12i 5738 oveq12d 5744 oveqan12d 5745 ecopoveq 6476 ecopovtrn 6478 ecopovtrng 6481 th3qlem1 6483 th3qlem2 6484 mulcmpblnq 7118 addpipqqs 7120 ordpipqqs 7124 enq0breq 7186 mulcmpblnq0 7194 nqpnq0nq 7203 nqnq0a 7204 nqnq0m 7205 nq0m0r 7206 nq0a0 7207 distrlem5prl 7336 distrlem5pru 7337 addcmpblnr 7476 ltsrprg 7484 mulgt0sr 7514 add20 8149 cru 8276 qaddcl 9323 qmulcl 9325 xaddval 9515 xnn0xadd0 9537 fzopth 9728 modqval 9984 seqvalcd 10119 seqovcd 10123 1exp 10209 m1expeven 10227 nn0opthd 10355 faclbnd 10374 faclbnd3 10376 bcn0 10388 reval 10508 absval 10659 clim 10936 fsumparts 11125 dvds2add 11369 dvds2sub 11370 opoe 11434 omoe 11435 opeo 11436 omeo 11437 gcddvds 11494 gcdcl 11497 gcdeq0 11507 gcdneg 11512 gcdaddm 11514 gcdabs 11518 gcddiv 11547 eucalgval2 11574 lcmabs 11597 rpmul 11619 divgcdcoprmex 11623 prmexpb 11669 rpexp 11671 nn0gcdsq 11717 cnmpt2t 12298 cnmpt22f 12300 bdmetval 12483 |
Copyright terms: Public domain | W3C validator |