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 6667 | . 2 ⊢ (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
3 | 2 | adantr 481 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 (class class class)co 6650 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 |
This theorem is referenced by: fullresc 16511 fucpropd 16637 resssetc 16742 resscatc 16755 issstrmgm 17252 gsumpropd 17272 grpsubpropd 17520 sylow2blem2 18036 isringd 18585 prdsringd 18612 prdscrngd 18613 prds1 18614 pwsco1rhm 18738 pwsco2rhm 18739 pwsdiagrhm 18813 sralmod 19187 sralmod0 19188 issubrngd2 19189 isdomn 19294 sraassa 19325 opsrcrng 19488 opsrassa 19489 ply1lss 19566 ply1subrg 19567 opsr0 19588 opsr1 19589 subrgply1 19603 opsrring 19615 opsrlmod 19616 ply1mpl0 19625 ply1mpl1 19627 ply1ascl 19628 coe1tm 19643 evls1rhm 19687 evl1rhm 19696 evl1expd 19709 znzrh 19891 zncrng 19893 mat0 20223 matinvg 20224 matlmod 20235 scmatsrng1 20329 1mavmul 20354 mat2pmatmul 20536 ressprdsds 22176 nmpropd 22398 tng0 22447 tngngp2 22456 tnggrpr 22459 tngnrg 22478 sranlm 22488 tchphl 23026 istrkgc 25353 istrkgb 25354 abvpropd2 29652 resv0g 29836 resvcmn 29838 zhmnrg 30011 prdsbnd 33592 prdstotbnd 33593 prdsbnd2 33594 erngdvlem3 36278 erngdvlem3-rN 36286 hlhils0 37237 hlhils1N 37238 hlhillvec 37243 hlhildrng 37244 hlhil0 37247 hlhillsm 37248 mendval 37753 issubmgm2 41790 rnghmval 41891 lidlmmgm 41925 rnghmsubcsetclem1 41975 rnghmsubcsetclem2 41976 rngcifuestrc 41997 rhmsubcsetclem1 42021 rhmsubcsetclem2 42022 rhmsubcrngclem1 42027 rhmsubcrngclem2 42028 |
Copyright terms: Public domain | W3C validator |