![]() |
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 7435 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | syl2an 594 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 (class class class)co 7426 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4916 df-br 5156 df-iota 6508 df-fv 6564 df-ov 7429 |
This theorem is referenced by: oveqan12rd 7446 offval 7701 offval3 7998 odi 8611 omopth2 8616 oeoa 8629 ecovdi 8856 ackbij1lem9 10273 distrpi 10943 addpipq 10982 mulpipq 10985 lterpq 11015 reclem3pr 11094 1idsr 11143 mulcnsr 11181 mulrid 11264 1re 11266 mul02 11444 addcom 11452 mulsub 11709 mulsub2 11710 muleqadd 11910 divmuldiv 11967 div2sub 12092 addltmul 12502 xnegdi 13283 xadddilem 13329 fzsubel 13593 fzoval 13689 seqid3 14068 mulexp 14123 sqdiv 14142 hashdom 14398 hashun 14401 ccatfval 14583 splcl 14762 crim 15122 readd 15133 remullem 15135 imadd 15141 cjadd 15148 cjreim 15167 sqrtmul 15266 sqabsadd 15289 sqabssub 15290 absmul 15301 abs2dif 15339 bhmafibid1 15472 binom 15836 binomfallfac 16045 sinadd 16168 cosadd 16169 dvds2ln 16293 sadcaddlem 16459 bezoutlem4 16545 bezout 16546 absmulgcd 16552 gcddiv 16554 bezoutr1 16572 lcmgcd 16610 lcmfass 16649 nn0gcdsq 16756 crth 16782 pythagtriplem1 16820 pcqmul 16857 4sqlem4a 16955 4sqlem4 16956 prdsplusgval 17490 prdsmulrval 17492 prdsdsval 17495 prdsvscaval 17496 idmgmhm 18696 resmgmhm 18706 idmhm 18787 0mhm 18811 resmhm 18812 prdspjmhm 18821 pwsdiagmhm 18823 gsumws2 18834 frmdup1 18856 eqgval 19173 idghm 19227 resghm 19228 mulgmhm 19827 mulgghm 19828 srglmhm 20206 srgrmhm 20207 ringlghm 20293 ringrghm 20294 gsumdixp 20300 isrhm 20462 rhmval 20484 issrngd 20836 lmodvsghm 20901 pwssplit2 21040 xrsdsval 21409 expmhm 21435 expghm 21467 mulgghm2 21468 mulgrhm 21469 pzriprnglem4 21476 cygznlem3 21569 asclghm 21882 psrmulfval 21954 evlslem4 22091 mpfrcl 22102 mamuval 22387 mamufv 22388 mvmulval 22539 mndifsplit 22632 mat2pmatmul 22727 decpmatmul 22768 fmval 23941 fmf 23943 flffval 23987 divcnOLD 24878 divcn 24880 rescncf 24911 htpyco1 24998 tcphcph 25259 rrxdsfival 25435 ehl2eudisval 25445 volun 25568 dyadval 25615 dvlip 26020 ftc1a 26066 ftc2ditglem 26074 tdeglem3 26087 tdeglem3OLD 26088 q1pval 26185 reefgim 26483 relogoprlem 26621 eflogeq 26632 zetacvg 27046 lgsdir2 27362 lgsdchr 27387 2sq2 27465 2sqnn0 27470 negsdi 28062 brbtwn2 28842 ax5seglem4 28869 axeuclid 28900 axcontlem2 28902 axcontlem4 28904 axcontlem8 28908 clwwlknccat 29999 ex-fpar 30398 ipasslem11 30776 hhssnv 31200 mayete3i 31664 idunop 31914 idhmop 31918 0lnfn 31921 lnopmi 31936 lnophsi 31937 lnopcoi 31939 hmops 31956 hmopm 31957 nlelshi 31996 cnlnadjlem2 32004 kbass6 32057 strlem3a 32188 hstrlem3a 32196 mndpluscn 33743 xrge0iifhom 33754 rezh 33788 probdsb 34258 resconn 35076 iscvm 35089 satfdmlem 35198 satffunlem1lem1 35232 satffunlem2lem1 35234 fwddifnval 35989 bj-bary1 37021 poimirlem15 37338 mbfposadd 37370 ftc1anclem3 37398 rrnmval 37531 dvhopaddN 40815 nnadddir 41989 cnreeu 42161 prjcrvfval 42301 pellex 42510 rmxfval 42579 rmyfval 42580 qirropth 42583 rmxycomplete 42593 jm2.15nn0 42679 rmxdioph 42692 expdiophlem2 42698 mendvsca 42870 deg1mhm 42883 mnringmulrvald 43919 addrval 44158 subrval 44159 fmulcl 45220 fmuldfeqlem1 45221 line 48138 itsclc0xyqsolr 48175 |
Copyright terms: Public domain | W3C validator |