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 6568 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
4 | 3 | ancoms 468 | 1 ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 (class class class)co 6549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 |
This theorem is referenced by: addpipq 9638 mulgt0sr 9805 mulcnsr 9836 mulresr 9839 recdiv 10610 revccat 13366 rlimdiv 14224 caucvg 14257 divgcdcoprm0 15217 estrchom 16590 funcestrcsetclem5 16607 ismhm 17160 mpfrcl 19339 xrsdsval 19609 matval 20036 ucnval 21891 volcn 23180 dvres2lem 23480 dvid 23487 c1lip3 23566 taylthlem1 23931 abelthlem9 23998 brbtwn2 25585 nonbooli 27894 0cnop 28222 0cnfn 28223 idcnop 28224 bccolsum 30878 ftc1anc 32663 rmydioph 36599 expdiophlem2 36607 dvcosax 38816 ismgmhm 41573 2zrngamgm 41729 rnghmsscmap2 41765 rnghmsscmap 41766 funcrngcsetc 41790 rhmsscmap2 41811 rhmsscmap 41812 funcringcsetc 41827 |
Copyright terms: Public domain | W3C validator |