![]() |
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 7410 | . 2 ⊢ (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
3 | 2 | adantr 481 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = 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-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3951 df-ss 3961 df-uni 4902 df-br 5142 df-iota 6484 df-fv 6540 df-ov 7396 |
This theorem is referenced by: fullresc 17783 fucpropd 17912 resssetc 18024 resscatc 18041 issstrmgm 18554 gsumpropd 18579 grpsubpropd 18902 sylow2blem2 19453 isringd 20062 prdsringd 20089 prdscrngd 20090 prds1 20091 pwsco1rhm 20227 pwsco2rhm 20228 pwsdiagrhm 20348 primefld 20370 sralmod 20757 sralmod0 20758 issubrngd2 20759 isdomn 20846 znzrh 21031 zncrng 21033 phlssphl 21145 sraassa 21355 opsrcrng 21548 opsrassa 21549 ply1lss 21649 ply1subrg 21650 opsr0 21671 opsr1 21672 subrgply1 21686 opsrring 21698 opsrlmod 21699 ply1mpl0 21708 ply1mpl1 21710 ply1ascl 21711 coe1tm 21726 evls1rhm 21770 evl1rhm 21780 evl1expd 21793 mat0 21848 matinvg 21849 matlmod 21860 scmatsrng1 21954 1mavmul 21979 mat2pmatmul 22162 ressprdsds 23806 nmpropd 24032 tng0 24084 tngngp2 24098 tnggrpr 24101 tngnrg 24120 sranlm 24130 pi1addval 24493 cvsi 24575 tcphphl 24673 abvpropd2 32000 resv0g 32317 resvcmn 32319 sra1r 32508 sraring 32509 sradrng 32510 srasubrg 32511 drgextlsp 32518 tnglvec 32533 tngdim 32534 matdim 32536 fedgmullem2 32551 evls1maplmhm 32595 zhmnrg 32776 prdsbnd 36464 prdstotbnd 36465 prdsbnd2 36466 erngdvlem3 39664 erngdvlem3-rN 39672 hlhils0 40623 hlhils1N 40624 hlhillvec 40629 hlhildrng 40630 hlhil0 40633 hlhillsm 40634 mendval 41694 mnring0gd 42747 mnringlmodd 42754 issubmgm2 46330 rnghmval 46435 lidlmmgm 46469 rnghmsubcsetclem1 46519 rnghmsubcsetclem2 46520 rngcifuestrc 46541 rhmsubcsetclem1 46565 rhmsubcsetclem2 46566 rhmsubcrngclem1 46571 rhmsubcrngclem2 46572 |
Copyright terms: Public domain | W3C validator |