![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > oveq123d | Structured version Visualization version GIF version |
Description: Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
Ref | Expression |
---|---|
oveq123d.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
oveq123d.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
oveq123d.3 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
oveq123d | ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq123d.1 | . . 3 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | 1 | oveqd 7410 | . 2 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐴𝐺𝐶)) |
3 | oveq123d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | oveq123d.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
5 | 3, 4 | oveq12d 7411 | . 2 ⊢ (𝜑 → (𝐴𝐺𝐶) = (𝐵𝐺𝐷)) |
6 | 2, 5 | eqtrd 2771 | 1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 (class class class)co 7393 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-iota 6484 df-fv 6540 df-ov 7396 |
This theorem is referenced by: csbov123 7435 prdsplusgfval 17402 prdsmulrfval 17404 prdsvscafval 17408 prdsdsval2 17412 xpsaddlem 17501 xpsvsca 17505 iscat 17598 iscatd 17599 iscatd2 17607 catcocl 17611 catass 17612 moni 17665 rcaninv 17723 subccocl 17777 isfunc 17796 funcco 17803 idfucl 17813 cofuval 17814 cofuval2 17819 cofucl 17820 funcres 17828 ressffth 17871 isnat 17880 nati 17888 fuccoval 17898 coaval 18000 catcisolem 18042 xpcco 18117 xpcco2 18121 1stfcl 18131 2ndfcl 18132 prfcl 18137 evlf2 18153 evlfcllem 18156 evlfcl 18157 curfval 18158 curf1 18160 curf12 18162 curf1cl 18163 curf2 18164 curf2val 18165 curf2cl 18166 curfcl 18167 uncfcurf 18174 hofval 18187 hof2fval 18190 hofcl 18194 yonedalem4a 18210 yonedalem3 18215 yonedainv 18216 isdlat 18457 issgrp 18593 ismndd 18624 grpsubfval 18843 grpsubfvalALT 18844 grpsubpropd 18902 imasgrp 18913 subgsub 18990 eqgfval 19028 dpjfval 19884 issrg 19969 isring 20018 isringd 20062 dvrfval 20166 isdrngd 20297 isdrngdOLD 20299 issrngd 20418 islmodd 20426 isphld 21140 phlssphl 21145 pjfval 21194 islindf 21300 isassa 21344 isassad 21352 asclfval 21364 ressascl 21381 psrval 21399 coe1tm 21726 evl1varpw 21809 scmatval 21935 mdetfval 22017 smadiadetr 22106 pmatcollpw2lem 22208 pm2mpval 22226 pm2mpghm 22247 chpmatfval 22261 cpmadugsumlemB 22305 xkohmeo 23248 xpsdsval 23816 prdsxmslem2 23967 nmfval 24026 nmpropd 24032 nmpropd2 24033 subgnm 24071 tngnm 24097 cph2di 24653 cphassr 24658 ipcau2 24680 tcphcphlem2 24682 rrxplusgvscavalb 24841 q1pval 25600 r1pval 25603 dvntaylp 25812 israg 27813 ttgval 27991 ttgvalOLD 27992 grpodivfval 29650 dipfval 29818 lnoval 29868 ressnm 31999 isslmd 32218 idlinsubrg 32400 fedgmullem2 32553 evls1maplmhm 32597 qqhval 32785 sitgval 33162 rdgeqoa 36055 prdsbnd2 36468 isrngo 36570 lflset 37734 islfld 37737 ldualset 37800 cmtfvalN 37885 isoml 37913 ltrnfset 38793 trlfset 38836 docaffvalN 39797 diblss 39846 dihffval 39906 dihfval 39907 hvmapffval 40434 hvmapfval 40435 hgmapfval 40562 imacrhmcl 40893 mendval 41696 hoidmvlelem3 45086 hspmbllem2 45116 isasslaw 46374 isrng 46422 lidlmsgrp 46472 lidlrng 46473 zlmodzxzscm 46681 lcoop 46740 lincvalsng 46745 lincvalpr 46747 lincdifsn 46753 islininds 46775 lines 47065 mndtchom 47358 mndtcco 47359 mndtccatid 47361 |
Copyright terms: Public domain | W3C validator |