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 7293 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | syl2an 596 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1539 (class class class)co 7284 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5076 df-iota 6395 df-fv 6445 df-ov 7287 |
This theorem is referenced by: oveqan12rd 7304 offval 7551 offval3 7834 odi 8419 omopth2 8424 oeoa 8437 ecovdi 8623 ackbij1lem9 9993 distrpi 10663 addpipq 10702 mulpipq 10705 lterpq 10735 reclem3pr 10814 1idsr 10863 mulcnsr 10901 mulid1 10982 1re 10984 mul02 11162 addcom 11170 mulsub 11427 mulsub2 11428 muleqadd 11628 divmuldiv 11684 div2sub 11809 addltmul 12218 xnegdi 12991 xadddilem 13037 fzsubel 13301 fzoval 13397 seqid3 13776 mulexp 13831 sqdiv 13850 hashdom 14103 hashun 14106 ccatfval 14285 splcl 14474 crim 14835 readd 14846 remullem 14848 imadd 14854 cjadd 14861 cjreim 14880 sqrtmul 14980 sqabsadd 15003 sqabssub 15004 absmul 15015 abs2dif 15053 bhmafibid1 15186 binom 15551 binomfallfac 15760 sinadd 15882 cosadd 15883 dvds2ln 16007 sadcaddlem 16173 bezoutlem4 16259 bezout 16260 absmulgcd 16266 gcddiv 16268 bezoutr1 16283 lcmgcd 16321 lcmfass 16360 nn0gcdsq 16465 crth 16488 pythagtriplem1 16526 pcqmul 16563 4sqlem4a 16661 4sqlem4 16662 prdsplusgval 17193 prdsmulrval 17195 prdsdsval 17198 prdsvscaval 17199 idmhm 18448 0mhm 18467 resmhm 18468 prdspjmhm 18476 pwsdiagmhm 18478 gsumws2 18490 frmdup1 18512 eqgval 18814 idghm 18858 resghm 18859 mulgmhm 19438 mulgghm 19439 srglmhm 19780 srgrmhm 19781 ringlghm 19852 ringrghm 19853 gsumdixp 19857 isrhm 19974 issrngd 20130 lmodvsghm 20193 pwssplit2 20331 xrsdsval 20651 expmhm 20676 expghm 20706 mulgghm2 20707 mulgrhm 20708 cygznlem3 20786 asclghm 21096 psrmulfval 21163 evlslem4 21293 mpfrcl 21304 mamuval 21544 mamufv 21545 mvmulval 21701 mndifsplit 21794 mat2pmatmul 21889 decpmatmul 21930 fmval 23103 fmf 23105 flffval 23149 divcn 24040 rescncf 24069 htpyco1 24150 tcphcph 24410 rrxdsfival 24586 ehl2eudisval 24596 volun 24718 dyadval 24765 dvlip 25166 ftc1a 25210 ftc2ditglem 25218 tdeglem3 25231 tdeglem3OLD 25232 q1pval 25327 reefgim 25618 relogoprlem 25755 eflogeq 25766 zetacvg 26173 lgsdir2 26487 lgsdchr 26512 2sq2 26590 2sqnn0 26595 brbtwn2 27282 ax5seglem4 27309 axeuclid 27340 axcontlem2 27342 axcontlem4 27344 axcontlem8 27348 clwwlknccat 28436 ex-fpar 28835 ipasslem11 29211 hhssnv 29635 mayete3i 30099 idunop 30349 idhmop 30353 0lnfn 30356 lnopmi 30371 lnophsi 30372 lnopcoi 30374 hmops 30391 hmopm 30392 nlelshi 30431 cnlnadjlem2 30439 kbass6 30492 strlem3a 30623 hstrlem3a 30631 mndpluscn 31885 xrge0iifhom 31896 rezh 31930 probdsb 32398 resconn 33217 iscvm 33230 satfdmlem 33339 satffunlem1lem1 33373 satffunlem2lem1 33375 fwddifnval 34474 bj-bary1 35492 poimirlem15 35801 mbfposadd 35833 ftc1anclem3 35861 rrnmval 35995 dvhopaddN 39135 nnadddir 40307 cnreeu 40445 prjcrvfval 40475 pellex 40664 rmxfval 40733 rmyfval 40734 qirropth 40737 rmxycomplete 40746 jm2.15nn0 40832 rmxdioph 40845 expdiophlem2 40851 mendvsca 41023 deg1mhm 41039 mnringmulrvald 41852 addrval 42091 subrval 42092 fmulcl 43129 fmuldfeqlem1 43130 idmgmhm 45353 resmgmhm 45363 rhmval 45488 line 46089 itsclc0xyqsolr 46126 |
Copyright terms: Public domain | W3C validator |