![]() |
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 5904 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2an 289 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-rex 2474 df-v 2754 df-un 3148 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-br 4019 df-iota 5196 df-fv 5243 df-ov 5898 |
This theorem is referenced by: oveqan12rd 5915 offval 6113 offval3 6158 ecovdi 6671 ecovidi 6672 distrpig 7361 addcmpblnq 7395 addpipqqs 7398 mulpipq 7400 addcomnqg 7409 addcmpblnq0 7471 distrnq0 7487 recexprlem1ssl 7661 recexprlem1ssu 7662 1idsr 7796 addcnsrec 7870 mulcnsrec 7871 mulrid 7983 mulsub 8387 mulsub2 8388 muleqadd 8654 divmuldivap 8698 div2subap 8823 addltmul 9184 xnegdi 9897 fzsubel 10089 fzoval 10177 mulexp 10589 sqdivap 10614 crim 10898 readd 10909 remullem 10911 imadd 10917 cjadd 10924 cjreim 10943 sqrtmul 11075 sqabsadd 11095 sqabssub 11096 absmul 11109 abs2dif 11146 binom 11523 sinadd 11775 cosadd 11776 dvds2ln 11862 absmulgcd 12049 gcddiv 12051 bezoutr1 12065 lcmgcd 12109 nn0gcdsq 12231 crth 12255 pythagtriplem1 12296 pcqmul 12334 4sqlem4a 12422 4sqlem4 12423 idmhm 12918 resmhm 12936 eqgval 13159 idghm 13195 resghm 13196 isrhm 13505 rhmval 13520 xmetxp 14459 xmetxpbl 14460 txmetcnp 14470 divcnap 14507 rescncf 14520 relogoprlem 14741 lgsdir2 14887 |
Copyright terms: Public domain | W3C validator |