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 7157 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | syl2an 597 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1531 (class class class)co 7148 |
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 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-rex 3142 df-rab 3145 df-v 3495 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7151 |
This theorem is referenced by: oveqan12rd 7168 offval 7408 offval3 7675 odi 8197 omopth2 8202 oeoa 8215 ecovdi 8397 ackbij1lem9 9642 distrpi 10312 addpipq 10351 mulpipq 10354 lterpq 10384 reclem3pr 10463 1idsr 10512 mulcnsr 10550 mulid1 10631 1re 10633 mul02 10810 addcom 10818 mulsub 11075 mulsub2 11076 muleqadd 11276 divmuldiv 11332 div2sub 11457 addltmul 11865 xnegdi 12633 xadddilem 12679 fzsubel 12935 fzoval 13031 seqid3 13406 mulexp 13460 sqdiv 13479 hashdom 13732 hashun 13735 ccatfval 13917 splcl 14106 crim 14466 readd 14477 remullem 14479 imadd 14485 cjadd 14492 cjreim 14511 sqrtmul 14611 sqabsadd 14634 sqabssub 14635 absmul 14646 abs2dif 14684 bhmafibid1 14817 binom 15177 binomfallfac 15387 sinadd 15509 cosadd 15510 dvds2ln 15634 sadcaddlem 15798 bezoutlem4 15882 bezout 15883 absmulgcd 15889 gcddiv 15891 bezoutr1 15905 lcmgcd 15943 lcmfass 15982 nn0gcdsq 16084 crth 16107 pythagtriplem1 16145 pcqmul 16182 4sqlem4a 16279 4sqlem4 16280 prdsplusgval 16738 prdsmulrval 16740 prdsdsval 16743 prdsvscaval 16744 idmhm 17957 0mhm 17976 resmhm 17977 prdspjmhm 17985 pwsdiagmhm 17987 gsumws2 17999 frmdup1 18021 eqgval 18321 idghm 18365 resghm 18366 mulgmhm 18940 mulgghm 18941 srglmhm 19277 srgrmhm 19278 ringlghm 19346 ringrghm 19347 gsumdixp 19351 isrhm 19465 issrngd 19624 lmodvsghm 19687 pwssplit2 19824 asclghm 20104 psrmulfval 20157 evlslem4 20280 mpfrcl 20290 xrsdsval 20581 expmhm 20606 expghm 20635 mulgghm2 20636 mulgrhm 20637 cygznlem3 20708 mamuval 20989 mamufv 20990 mvmulval 21144 mndifsplit 21237 mat2pmatmul 21331 decpmatmul 21372 fmval 22543 fmf 22545 flffval 22589 divcn 23468 rescncf 23497 htpyco1 23574 tcphcph 23832 rrxdsfival 24008 ehl2eudisval 24018 volun 24138 dyadval 24185 dvlip 24582 ftc1a 24626 ftc2ditglem 24634 tdeglem3 24645 q1pval 24739 reefgim 25030 relogoprlem 25166 eflogeq 25177 zetacvg 25584 lgsdir2 25898 lgsdchr 25923 2sq2 26001 2sqnn0 26006 brbtwn2 26683 ax5seglem4 26710 axeuclid 26741 axcontlem2 26743 axcontlem4 26745 axcontlem8 26749 clwwlknccat 27834 ex-fpar 28233 ipasslem11 28609 hhssnv 29033 mayete3i 29497 idunop 29747 idhmop 29751 0lnfn 29754 lnopmi 29769 lnophsi 29770 lnopcoi 29772 hmops 29789 hmopm 29790 nlelshi 29829 cnlnadjlem2 29837 kbass6 29890 strlem3a 30021 hstrlem3a 30029 mndpluscn 31162 xrge0iifhom 31173 rezh 31205 probdsb 31673 resconn 32486 iscvm 32499 satfdmlem 32608 satffunlem1lem1 32642 satffunlem2lem1 32644 fwddifnval 33617 bj-bary1 34585 poimirlem15 34899 mbfposadd 34931 ftc1anclem3 34961 rrnmval 35098 dvhopaddN 38242 nnadddir 39154 pellex 39423 rmxfval 39492 rmyfval 39493 qirropth 39496 rmxycomplete 39505 jm2.15nn0 39591 rmxdioph 39604 expdiophlem2 39610 mendvsca 39782 deg1mhm 39798 addrval 40789 subrval 40790 fmulcl 41852 fmuldfeqlem1 41853 idmgmhm 44046 resmgmhm 44056 rhmval 44181 line 44710 itsclc0xyqsolr 44747 |
Copyright terms: Public domain | W3C validator |