| 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 7440 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
| 4 | 1, 2, 3 | syl2an 596 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 (class class class)co 7431 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 |
| This theorem is referenced by: oveqan12rd 7451 offval 7706 offval3 8007 odi 8617 omopth2 8622 oeoa 8635 ecovdi 8865 ackbij1lem9 10267 distrpi 10938 addpipq 10977 mulpipq 10980 lterpq 11010 reclem3pr 11089 1idsr 11138 mulcnsr 11176 mulrid 11259 1re 11261 mul02 11439 addcom 11447 mulsub 11706 mulsub2 11707 muleqadd 11907 divmuldiv 11967 div2sub 12092 addltmul 12502 xnegdi 13290 xadddilem 13336 fzsubel 13600 fzoval 13700 seqid3 14087 mulexp 14142 sqdiv 14161 hashdom 14418 hashun 14421 ccatfval 14611 splcl 14790 crim 15154 readd 15165 remullem 15167 imadd 15173 cjadd 15180 cjreim 15199 sqrtmul 15298 sqabsadd 15321 sqabssub 15322 absmul 15333 abs2dif 15371 bhmafibid1 15504 binom 15866 binomfallfac 16077 sinadd 16200 cosadd 16201 dvds2ln 16326 sadcaddlem 16494 bezoutlem4 16579 bezout 16580 absmulgcd 16586 gcddiv 16588 bezoutr1 16606 lcmgcd 16644 lcmfass 16683 nn0gcdsq 16789 crth 16815 pythagtriplem1 16854 pcqmul 16891 4sqlem4a 16989 4sqlem4 16990 prdsplusgval 17518 prdsmulrval 17520 prdsdsval 17523 prdsvscaval 17524 idmgmhm 18714 resmgmhm 18724 idmhm 18808 0mhm 18832 resmhm 18833 prdspjmhm 18842 pwsdiagmhm 18844 gsumws2 18855 frmdup1 18877 eqgval 19195 idghm 19249 resghm 19250 mulgmhm 19845 mulgghm 19846 srglmhm 20218 srgrmhm 20219 ringlghm 20309 ringrghm 20310 gsumdixp 20316 isrhm 20478 rhmval 20500 issrngd 20856 lmodvsghm 20921 pwssplit2 21059 xrsdsval 21428 expmhm 21454 expghm 21486 mulgghm2 21487 mulgrhm 21488 pzriprnglem4 21495 cygznlem3 21588 asclghm 21903 psrmulfval 21963 evlslem4 22100 mpfrcl 22109 mamuval 22397 mamufv 22398 mvmulval 22549 mndifsplit 22642 mat2pmatmul 22737 decpmatmul 22778 fmval 23951 fmf 23953 flffval 23997 divcnOLD 24890 divcn 24892 rescncf 24923 htpyco1 25010 tcphcph 25271 rrxdsfival 25447 ehl2eudisval 25457 volun 25580 dyadval 25627 dvlip 26032 ftc1a 26078 ftc2ditglem 26086 tdeglem3 26098 q1pval 26194 reefgim 26494 relogoprlem 26633 eflogeq 26644 zetacvg 27058 lgsdir2 27374 lgsdchr 27399 2sq2 27477 2sqnn0 27482 negsdi 28082 brbtwn2 28920 ax5seglem4 28947 axeuclid 28978 axcontlem2 28980 axcontlem4 28982 axcontlem8 28986 clwwlknccat 30082 ex-fpar 30481 ipasslem11 30859 hhssnv 31283 mayete3i 31747 idunop 31997 idhmop 32001 0lnfn 32004 lnopmi 32019 lnophsi 32020 lnopcoi 32022 hmops 32039 hmopm 32040 nlelshi 32079 cnlnadjlem2 32087 kbass6 32140 strlem3a 32271 hstrlem3a 32279 elrgspnlem2 33247 mndpluscn 33925 xrge0iifhom 33936 rezh 33970 probdsb 34424 resconn 35251 iscvm 35264 satfdmlem 35373 satffunlem1lem1 35407 satffunlem2lem1 35409 fwddifnval 36164 bj-bary1 37313 poimirlem15 37642 mbfposadd 37674 ftc1anclem3 37702 rrnmval 37835 dvhopaddN 41116 nnadddir 42305 cnreeu 42500 prjcrvfval 42641 pellex 42846 rmxfval 42915 rmyfval 42916 qirropth 42919 rmxycomplete 42929 jm2.15nn0 43015 rmxdioph 43028 expdiophlem2 43034 mendvsca 43199 deg1mhm 43212 mnringmulrvald 44246 addrval 44485 subrval 44486 fmulcl 45596 fmuldfeqlem1 45597 line 48653 itsclc0xyqsolr 48690 |
| Copyright terms: Public domain | W3C validator |