![]() |
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 7016 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | syl2an 595 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1520 (class class class)co 7007 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-rex 3109 df-rab 3112 df-v 3434 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-br 4957 df-iota 6181 df-fv 6225 df-ov 7010 |
This theorem is referenced by: oveqan12rd 7027 offval 7265 offval3 7530 odi 8046 omopth2 8051 oeoa 8064 ecovdi 8246 ackbij1lem9 9485 distrpi 10155 addpipq 10194 mulpipq 10197 lterpq 10227 reclem3pr 10306 1idsr 10355 mulcnsr 10393 mulid1 10474 1re 10476 mul02 10654 addcom 10662 mulsub 10920 mulsub2 10921 muleqadd 11121 divmuldiv 11177 div2sub 11302 addltmul 11710 xnegdi 12480 xadddilem 12526 fzsubel 12782 fzoval 12878 seqid3 13252 mulexp 13306 sqdiv 13325 hashdom 13576 hashun 13579 ccatfval 13759 splcl 13938 crim 14296 readd 14307 remullem 14309 imadd 14315 cjadd 14322 cjreim 14341 sqrtmul 14441 sqabsadd 14464 sqabssub 14465 absmul 14476 abs2dif 14514 bhmafibid1 14647 binom 15006 binomfallfac 15216 sinadd 15338 cosadd 15339 dvds2ln 15463 sadcaddlem 15627 bezoutlem4 15707 bezout 15708 absmulgcd 15714 gcddiv 15716 bezoutr1 15730 lcmgcd 15768 lcmfass 15807 nn0gcdsq 15909 crth 15932 pythagtriplem1 15970 pcqmul 16007 4sqlem4a 16104 4sqlem4 16105 prdsplusgval 16563 prdsmulrval 16565 prdsdsval 16568 prdsvscaval 16569 idmhm 17771 0mhm 17785 resmhm 17786 prdspjmhm 17794 pwsdiagmhm 17796 gsumws2 17806 frmdup1 17828 eqgval 18070 idghm 18102 resghm 18103 mulgmhm 18661 mulgghm 18662 srglmhm 18963 srgrmhm 18964 ringlghm 19032 ringrghm 19033 gsumdixp 19037 isrhm 19151 issrngd 19310 lmodvsghm 19373 pwssplit2 19510 asclghm 19788 psrmulfval 19841 evlslem4 19963 mpfrcl 19973 xrsdsval 20259 expmhm 20284 expghm 20313 mulgghm2 20314 mulgrhm 20315 cygznlem3 20386 mamuval 20667 mamufv 20668 mvmulval 20824 mndifsplit 20917 mat2pmatmul 21011 decpmatmul 21052 fmval 22223 fmf 22225 flffval 22269 divcn 23147 rescncf 23176 htpyco1 23253 tcphcph 23511 rrxdsfival 23687 ehl2eudisval 23697 volun 23817 dyadval 23864 dvlip 24261 ftc1a 24305 ftc2ditglem 24313 tdeglem3 24324 q1pval 24418 reefgim 24709 relogoprlem 24843 eflogeq 24854 zetacvg 25262 lgsdir2 25576 lgsdchr 25601 2sq2 25679 2sqnn0 25684 brbtwn2 26362 ax5seglem4 26389 axeuclid 26420 axcontlem2 26422 axcontlem4 26424 axcontlem8 26428 clwwlknccat 27517 ipasslem11 28296 hhssnv 28720 mayete3i 29184 idunop 29434 idhmop 29438 0lnfn 29441 lnopmi 29456 lnophsi 29457 lnopcoi 29459 hmops 29476 hmopm 29477 nlelshi 29516 cnlnadjlem2 29524 kbass6 29577 strlem3a 29708 hstrlem3a 29716 mndpluscn 30742 xrge0iifhom 30753 rezh 30785 probdsb 31253 resconn 32057 iscvm 32070 satfdmlem 32177 satffunlem1lem1 32210 satffunlem2lem1 32212 fwddifnval 33178 bj-bary1 34076 poimirlem15 34384 mbfposadd 34416 ftc1anclem3 34446 rrnmval 34584 dvhopaddN 37731 pellex 38868 rmxfval 38937 rmyfval 38938 qirropth 38941 rmxycomplete 38950 jm2.15nn0 39036 rmxdioph 39049 expdiophlem2 39055 mendvsca 39227 deg1mhm 39243 addrval 40289 subrval 40290 fmulcl 41358 fmuldfeqlem1 41359 idmgmhm 43491 resmgmhm 43501 rhmval 43622 offval0 43999 line 44154 itsclc0xyqsolr 44191 |
Copyright terms: Public domain | W3C validator |