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 6558 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | syl2an 493 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 (class class class)co 6549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 |
This theorem is referenced by: oveqan12rd 6569 offval 6802 offval3 7053 odi 7546 omopth2 7551 oeoa 7564 ecovdi 7743 ackbij1lem9 8933 alephadd 9278 distrpi 9599 addpipq 9638 mulpipq 9641 lterpq 9671 reclem3pr 9750 1idsr 9798 mulcnsr 9836 mulid1 9916 1re 9918 mul02 10093 addcom 10101 mulsub 10352 mulsub2 10353 muleqadd 10550 divmuldiv 10604 div2sub 10729 addltmul 11145 xnegdi 11950 xadddilem 11996 fzsubel 12248 fzoval 12340 seqid3 12707 mulexp 12761 sqdiv 12790 hashdom 13029 hashun 13032 ccatfval 13211 splcl 13354 crim 13703 readd 13714 remullem 13716 imadd 13722 cjadd 13729 cjreim 13748 sqrtmul 13848 sqabsadd 13870 sqabssub 13871 absmul 13882 abs2dif 13920 binom 14401 binomfallfac 14611 sinadd 14733 cosadd 14734 dvds2ln 14852 sadcaddlem 15017 bezoutlem4 15097 bezout 15098 absmulgcd 15104 gcddiv 15106 bezoutr1 15120 lcmgcd 15158 lcmfass 15197 nn0gcdsq 15298 crth 15321 pythagtriplem1 15359 pcqmul 15396 4sqlem4a 15493 4sqlem4 15494 prdsplusgval 15956 prdsmulrval 15958 prdsdsval 15961 prdsvscaval 15962 xpsfval 16050 xpsval 16055 idmhm 17167 0mhm 17181 resmhm 17182 prdspjmhm 17190 pwsdiagmhm 17192 gsumws2 17202 frmdup1 17224 eqgval 17466 idghm 17498 resghm 17499 mulgmhm 18056 mulgghm 18057 srglmhm 18358 srgrmhm 18359 ringlghm 18427 ringrghm 18428 gsumdixp 18432 isrhm 18544 issrngd 18684 lmodvsghm 18747 pwssplit2 18881 asclghm 19159 psrmulfval 19206 evlslem4 19329 mpfrcl 19339 xrsdsval 19609 expmhm 19634 expghm 19663 mulgghm2 19664 mulgrhm 19665 cygznlem3 19737 mamuval 20011 mamufv 20012 mvmulval 20168 mndifsplit 20261 mat2pmatmul 20355 decpmatmul 20396 fmval 21557 fmf 21559 flffval 21603 divcn 22479 rescncf 22508 htpyco1 22585 tchcph 22844 volun 23120 dyadval 23166 dvlip 23560 ftc1a 23604 ftc2ditglem 23612 tdeglem3 23623 q1pval 23717 reefgim 24008 relogoprlem 24141 eflogeq 24152 zetacvg 24541 lgsdir2 24855 lgsdchr 24880 brbtwn2 25585 ax5seglem4 25612 axeuclid 25643 axcontlem2 25645 axcontlem4 25647 axcontlem8 25651 numclwlk1lem2fo 26622 ipasslem11 27079 hhssnv 27505 mayete3i 27971 idunop 28221 idhmop 28225 0lnfn 28228 lnopmi 28243 lnophsi 28244 lnopcoi 28246 hmops 28263 hmopm 28264 nlelshi 28303 cnlnadjlem2 28311 kbass6 28364 strlem3a 28495 hstrlem3a 28503 bhmafibid1 28975 mndpluscn 29300 xrge0iifhom 29311 rezh 29343 probdsb 29811 rescon 30482 iscvm 30495 fwddifnval 31440 bj-bary1 32339 poimirlem15 32594 mbfposadd 32627 ftc1anclem3 32657 rrnmval 32797 dvhopaddN 35421 pellex 36417 rmxfval 36486 rmyfval 36487 qirropth 36491 rmxycomplete 36500 jm2.15nn0 36588 rmxdioph 36601 expdiophlem2 36607 mendvsca 36780 deg1mhm 36804 addrval 37691 subrval 37692 fmulcl 38648 fmuldfeqlem1 38649 av-numclwlk1lem2fo 41525 idmgmhm 41578 resmgmhm 41588 rhmval 41709 offval0 42093 |
Copyright terms: Public domain | W3C validator |