![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > oveqan12d | 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 |
---|---|
oveqan12d | ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | opreqan12i.2 | . 2 ⊢ (𝜓 → 𝐶 = 𝐷) | |
3 | oveq12 6822 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | syl2an 495 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 (class class class)co 6813 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-rex 3056 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-uni 4589 df-br 4805 df-iota 6012 df-fv 6057 df-ov 6816 |
This theorem is referenced by: oveqan12rd 6833 offval 7069 offval3 7327 odi 7828 omopth2 7833 oeoa 7846 ecovdi 8022 ackbij1lem9 9242 alephadd 9591 distrpi 9912 addpipq 9951 mulpipq 9954 lterpq 9984 reclem3pr 10063 1idsr 10111 mulcnsr 10149 mulid1 10229 1re 10231 mul02 10406 addcom 10414 mulsub 10665 mulsub2 10666 muleqadd 10863 divmuldiv 10917 div2sub 11042 addltmul 11460 xnegdi 12271 xadddilem 12317 fzsubel 12570 fzoval 12665 seqid3 13039 mulexp 13093 sqdiv 13122 hashdom 13360 hashun 13363 ccatfval 13545 splcl 13703 crim 14054 readd 14065 remullem 14067 imadd 14073 cjadd 14080 cjreim 14099 sqrtmul 14199 sqabsadd 14221 sqabssub 14222 absmul 14233 abs2dif 14271 binom 14761 binomfallfac 14971 sinadd 15093 cosadd 15094 dvds2ln 15216 sadcaddlem 15381 bezoutlem4 15461 bezout 15462 absmulgcd 15468 gcddiv 15470 bezoutr1 15484 lcmgcd 15522 lcmfass 15561 nn0gcdsq 15662 crth 15685 pythagtriplem1 15723 pcqmul 15760 4sqlem4a 15857 4sqlem4 15858 prdsplusgval 16335 prdsmulrval 16337 prdsdsval 16340 prdsvscaval 16341 xpsfval 16429 xpsval 16434 idmhm 17545 0mhm 17559 resmhm 17560 prdspjmhm 17568 pwsdiagmhm 17570 gsumws2 17580 frmdup1 17602 eqgval 17844 idghm 17876 resghm 17877 mulgmhm 18433 mulgghm 18434 srglmhm 18735 srgrmhm 18736 ringlghm 18804 ringrghm 18805 gsumdixp 18809 isrhm 18923 issrngd 19063 lmodvsghm 19126 pwssplit2 19262 asclghm 19540 psrmulfval 19587 evlslem4 19710 mpfrcl 19720 xrsdsval 19992 expmhm 20017 expghm 20046 mulgghm2 20047 mulgrhm 20048 cygznlem3 20120 mamuval 20394 mamufv 20395 mvmulval 20551 mndifsplit 20644 mat2pmatmul 20738 decpmatmul 20779 fmval 21948 fmf 21950 flffval 21994 divcn 22872 rescncf 22901 htpyco1 22978 tchcph 23236 volun 23513 dyadval 23560 dvlip 23955 ftc1a 23999 ftc2ditglem 24007 tdeglem3 24018 q1pval 24112 reefgim 24403 relogoprlem 24536 eflogeq 24547 zetacvg 24940 lgsdir2 25254 lgsdchr 25279 brbtwn2 25984 ax5seglem4 26011 axeuclid 26042 axcontlem2 26044 axcontlem4 26046 axcontlem8 26050 clwwlknccat 27194 ipasslem11 28004 hhssnv 28430 mayete3i 28896 idunop 29146 idhmop 29150 0lnfn 29153 lnopmi 29168 lnophsi 29169 lnopcoi 29171 hmops 29188 hmopm 29189 nlelshi 29228 cnlnadjlem2 29236 kbass6 29289 strlem3a 29420 hstrlem3a 29428 bhmafibid1 29953 mndpluscn 30281 xrge0iifhom 30292 rezh 30324 probdsb 30793 resconn 31535 iscvm 31548 fwddifnval 32576 bj-bary1 33473 poimirlem15 33737 mbfposadd 33770 ftc1anclem3 33800 rrnmval 33940 dvhopaddN 36905 pellex 37901 rmxfval 37970 rmyfval 37971 qirropth 37975 rmxycomplete 37984 jm2.15nn0 38072 rmxdioph 38085 expdiophlem2 38091 mendvsca 38263 deg1mhm 38287 addrval 39172 subrval 39173 fmulcl 40316 fmuldfeqlem1 40317 idmgmhm 42298 resmgmhm 42308 rhmval 42429 offval0 42809 |
Copyright terms: Public domain | W3C validator |