Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > oveqdr | Structured version Visualization version GIF version |
Description: Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.) |
Ref | Expression |
---|---|
oveqdr.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
Ref | Expression |
---|---|
oveqdr | ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveqdr.1 | . . 3 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | 1 | oveqd 7162 | . 2 ⊢ (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
3 | 2 | adantr 481 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 (class class class)co 7145 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rex 3141 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 |
This theorem is referenced by: fullresc 17109 fucpropd 17235 resssetc 17340 resscatc 17353 issstrmgm 17851 gsumpropd 17876 grpsubpropd 18142 sylow2blem2 18675 isringd 19264 prdsringd 19291 prdscrngd 19292 prds1 19293 pwsco1rhm 19419 pwsco2rhm 19420 pwsdiagrhm 19498 primefld 19513 sralmod 19888 sralmod0 19889 issubrngd2 19890 isdomn 19995 sraassa 20027 opsrcrng 20196 opsrassa 20197 ply1lss 20292 ply1subrg 20293 opsr0 20314 opsr1 20315 subrgply1 20329 opsrring 20341 opsrlmod 20342 ply1mpl0 20351 ply1mpl1 20353 ply1ascl 20354 coe1tm 20369 evls1rhm 20413 evl1rhm 20423 evl1expd 20436 znzrh 20617 zncrng 20619 phlssphl 20731 mat0 20954 matinvg 20955 matlmod 20966 scmatsrng1 21060 1mavmul 21085 mat2pmatmul 21267 ressprdsds 22908 nmpropd 23130 tng0 23179 tngngp2 23188 tnggrpr 23191 tngnrg 23210 sranlm 23220 pi1addval 23579 cvsi 23661 tcphphl 23757 istrkgc 26167 istrkgb 26168 abvpropd2 30566 resv0g 30836 resvcmn 30838 sra1r 30885 sraring 30886 sradrng 30887 srasubrg 30888 drgextlsp 30895 tnglvec 30909 tngdim 30910 matdim 30912 fedgmullem2 30925 zhmnrg 31107 prdsbnd 34952 prdstotbnd 34953 prdsbnd2 34954 erngdvlem3 38006 erngdvlem3-rN 38014 hlhils0 38961 hlhils1N 38962 hlhillvec 38967 hlhildrng 38968 hlhil0 38971 hlhillsm 38972 mendval 39661 issubmgm2 43934 rnghmval 44090 lidlmmgm 44124 rnghmsubcsetclem1 44174 rnghmsubcsetclem2 44175 rngcifuestrc 44196 rhmsubcsetclem1 44220 rhmsubcsetclem2 44221 rhmsubcrngclem1 44226 rhmsubcrngclem2 44227 |
Copyright terms: Public domain | W3C validator |