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 5521 | . 2 | |
4 | 1, 2, 3 | syl2an 273 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wceq 1243 (class class class)co 5512 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-3an 887 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-rex 2312 df-v 2559 df-un 2922 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-br 3765 df-iota 4867 df-fv 4910 df-ov 5515 |
This theorem is referenced by: oveqan12rd 5532 offval 5719 offval3 5761 ecovdi 6217 ecovidi 6218 distrpig 6431 addcmpblnq 6465 addpipqqs 6468 mulpipq 6470 addcomnqg 6479 addcmpblnq0 6541 distrnq0 6557 recexprlem1ssl 6731 recexprlem1ssu 6732 1idsr 6853 addcnsrec 6918 mulcnsrec 6919 mulid1 7024 mulsub 7398 mulsub2 7399 muleqadd 7649 divmuldivap 7688 addltmul 8161 fzsubel 8923 fzoval 9005 iseqid3 9245 mulexp 9294 sqdivap 9318 crim 9458 readd 9469 remullem 9471 imadd 9477 cjadd 9484 cjreim 9503 sqrtmul 9633 sqabsadd 9653 sqabssub 9654 absmul 9667 abs2dif 9702 |
Copyright terms: Public domain | W3C validator |