Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > oveqan12rd | Structured version Visualization version GIF version |
Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
oveq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
opreqan12i.2 | ⊢ (𝜓 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
oveqan12rd | ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | opreqan12i.2 | . . 3 ⊢ (𝜓 → 𝐶 = 𝐷) | |
3 | 1, 2 | oveqan12d 7164 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
4 | 3 | ancoms 459 | 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-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 |
This theorem is referenced by: addpipq 10347 mulgt0sr 10515 mulcnsr 10546 mulresr 10549 recdiv 11334 revccat 14116 rlimdiv 14990 caucvg 15023 divgcdcoprm0 15997 estrchom 17365 funcestrcsetclem5 17382 ismhm 17946 mpfrcl 20226 xrsdsval 20517 matval 20948 ucnval 22813 volcn 24134 dvres2lem 24435 dvid 24442 c1lip3 24523 taylthlem1 24888 abelthlem9 24955 2sqnn 25942 brbtwn2 26618 nonbooli 29355 0cnop 29683 0cnfn 29684 idcnop 29685 bccolsum 32868 ftc1anc 34856 rmydioph 39489 expdiophlem2 39497 dvcosax 42087 ismgmhm 43927 2zrngamgm 44138 rnghmsscmap2 44172 rnghmsscmap 44173 funcrngcsetc 44197 rhmsscmap2 44218 rhmsscmap 44219 funcringcsetc 44234 |
Copyright terms: Public domain | W3C validator |