Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > oveqan12d | Unicode version |
Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
oveq1d.1 | |
opreqan12i.2 |
Ref | Expression |
---|---|
oveqan12d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1d.1 | . 2 | |
2 | opreqan12i.2 | . 2 | |
3 | oveq12 5541 | . 2 | |
4 | 1, 2, 3 | syl2an 283 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 wceq 1284 (class class class)co 5532 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-3an 921 df-tru 1287 df-nf 1390 df-sb 1686 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-rex 2354 df-v 2603 df-un 2977 df-sn 3404 df-pr 3405 df-op 3407 df-uni 3602 df-br 3786 df-iota 4887 df-fv 4930 df-ov 5535 |
This theorem is referenced by: oveqan12rd 5552 offval 5739 offval3 5781 ecovdi 6240 ecovidi 6241 distrpig 6523 addcmpblnq 6557 addpipqqs 6560 mulpipq 6562 addcomnqg 6571 addcmpblnq0 6633 distrnq0 6649 recexprlem1ssl 6823 recexprlem1ssu 6824 1idsr 6945 addcnsrec 7010 mulcnsrec 7011 mulid1 7116 mulsub 7505 mulsub2 7506 muleqadd 7758 divmuldivap 7800 addltmul 8267 fzsubel 9078 fzoval 9158 iseqid3 9465 mulexp 9515 sqdivap 9540 crim 9745 readd 9756 remullem 9758 imadd 9764 cjadd 9771 cjreim 9790 sqrtmul 9921 sqabsadd 9941 sqabssub 9942 absmul 9955 abs2dif 9992 dvds2ln 10228 absmulgcd 10406 gcddiv 10408 bezoutr1 10422 lcmgcd 10460 |
Copyright terms: Public domain | W3C validator |