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 5862 | . 2 | |
4 | 1, 2, 3 | syl2an 287 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wceq 1348 (class class class)co 5853 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-rex 2454 df-v 2732 df-un 3125 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-br 3990 df-iota 5160 df-fv 5206 df-ov 5856 |
This theorem is referenced by: oveqan12rd 5873 offval 6068 offval3 6113 ecovdi 6624 ecovidi 6625 distrpig 7295 addcmpblnq 7329 addpipqqs 7332 mulpipq 7334 addcomnqg 7343 addcmpblnq0 7405 distrnq0 7421 recexprlem1ssl 7595 recexprlem1ssu 7596 1idsr 7730 addcnsrec 7804 mulcnsrec 7805 mulid1 7917 mulsub 8320 mulsub2 8321 muleqadd 8586 divmuldivap 8629 div2subap 8754 addltmul 9114 xnegdi 9825 fzsubel 10016 fzoval 10104 mulexp 10515 sqdivap 10540 crim 10822 readd 10833 remullem 10835 imadd 10841 cjadd 10848 cjreim 10867 sqrtmul 10999 sqabsadd 11019 sqabssub 11020 absmul 11033 abs2dif 11070 binom 11447 sinadd 11699 cosadd 11700 dvds2ln 11786 absmulgcd 11972 gcddiv 11974 bezoutr1 11988 lcmgcd 12032 nn0gcdsq 12154 crth 12178 pythagtriplem1 12219 pcqmul 12257 4sqlem4a 12343 4sqlem4 12344 idmhm 12692 xmetxp 13301 xmetxpbl 13302 txmetcnp 13312 divcnap 13349 rescncf 13362 relogoprlem 13583 lgsdir2 13728 |
Copyright terms: Public domain | W3C validator |