Theorem oveq12i 6854

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Hypotheses

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵
oveq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
oveq12i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Proof of Theorem oveq12i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		oveq12 6851	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	mp2an 683	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Syntax hints:   = wceq 1652  (class class class)co 6842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076  df-ov 6845

This theorem is referenced by:  oveq123i  6856  caovdir  7066  caovdilem  7067  caovlem2  7068  cnfcom2  8814  canthwelem  9725  adderpqlem  10029  addassnq  10033  distrnq  10036  ltanq  10046  1lt2nq  10048  ltexnq  10050  halfnq  10051  mulcmpblnrlem  10144  mulcomsr  10163  distrsr  10165  m1p1sr  10166  m1m1sr  10167  mulgt0sr  10179  addcnsrec  10217  mulcnsrec  10218  axmulcom  10229  axmulass  10231  axdistr  10232  axi2m1  10233  addid1  10470  3t3e9  11445  8th4div3  11498  halfpm6th  11499  numma  11785  decmul10add  11810  4t3lem  11838  9t11e99  11871  halfthird  11884  5recm6rec  11885  fz0to3un2pr  12649  seqfeq4  13057  seqof  13065  sqdivi  13155  sq4e2t8  13169  i4  13174  binom2i  13181  nn0opthlem1  13259  facp1  13269  fac2  13270  fac3  13271  fac4  13272  faclbnd4lem1  13284  4bc2eq6  13320  ccat2s1len  13596  ccat2s1p2  13604  cats1len  13891  cats2cat  13893  ofs2  13999  cji  14186  sqrlem5  14274  fsumadd  14757  fsumsplitf  14759  fsumsplitsnun  14771  fsumsplitsnunOLD  14773  0.999...  14898  fprodmul  14975  fproddiv  14976  fprodsplitf  15003  bpoly3  15073  fsumcube  15075  efsep  15124  ef01bndlem  15198  cos2bnd  15202  rpnnen2lem3  15229  3dvds2dec  15341  flodddiv4  15420  sadeq  15477  gcdaddmlem  15528  bezout  15543  nn0gcdsq  15741  pythagtriplem16  15816  4sqlem19  15948  dec5nprm  16051  dec2nprm  16052  mod2xnegi  16056  numexp2x  16064  decsplit  16068  karatsuba  16069  2exp16  16073  37prm  16103  43prm  16104  83prm  16105  139prm  16106  163prm  16107  317prm  16108  631prm  16109  1259lem1  16113  1259lem2  16114  1259lem3  16115  1259lem4  16116  1259lem5  16117  1259prm  16118  2503lem1  16119  2503lem2  16120  2503lem3  16121  2503prm  16122  4001lem1  16123  4001lem2  16124  4001lem3  16125  4001lem4  16126  4001prm  16127  funcoppc  16802  estrchom  17034  funcestrcsetclem5  17052  yonedalem3b  17187  gsum2dlem2  18636  opprring  18898  isrhm  18990  evlsval  19792  mamudi  20485  mamudir  20486  oftpos  20535  mamutpos  20541  mdetrlin  20685  mdetrlin2  20690  mdetunilem5  20699  cpmadugsumfi  20961  cnmpt2res  21760  ussval  22342  icopnfhmeo  23021  iccpnfhmeo  23023  pcoass  23102  ovolunlem1a  23554  ioombl1lem3  23618  ioombl1lem4  23619  mbfimaopnlem  23713  iblcnlem1  23845  itgfsum  23884  iblabslem  23885  itgsplit  23893  dveflem  24033  efhalfpi  24515  efipi  24517  sin2pi  24519  ef2pi  24521  sincosq3sgn  24544  sincosq4sgn  24545  sinq34lt0t  24553  sincos4thpi  24557  tan4thpi  24558  sincos6thpi  24559  sincos3rdpi  24560  pige3  24561  cxpcn3  24780  lawcos  24837  1cubrlem  24859  quart1lem  24873  quart1  24874  asin1  24912  atancj  24928  atanlogsublem  24933  log2cnv  24962  log2tlbnd  24963  log2ublem3  24966  log2ub  24967  birthday  24972  basellem8  25105  basellem9  25106  cht2  25189  cht3  25190  1sgm2ppw  25216  bclbnd  25296  bposlem8  25307  bposlem9  25308  lgsdi  25350  lgsquadlem1  25396  2lgsoddprmlem3c  25428  2lgsoddprmlem3d  25429  mirauto  25870  axsegconlem9  26096  ax5seglem7  26106  vtxdginducedm1  26730  clwlkclwwlkfo  27215  clwlksfoclwwlkOLD  27300  eupth2eucrct  27453  ex-exp  27701  ex-fac  27702  ex-bc  27703  ex-hash  27704  ip0i  28071  ip1ilem  28072  ip2i  28074  ipdirilem  28075  ipasslem10  28085  ip2dii  28090  pythi  28096  siilem1  28097  hvsubsub4i  28307  hvsubcan2i  28312  hisubcomi  28352  normlem0  28357  normlem1  28358  normlem2  28359  normlem3  28360  normlem6  28363  normlem8  28365  normlem9  28366  bcseqi  28368  norm-ii-i  28385  norm-iii-i  28387  normpythi  28390  norm3difi  28395  normpari  28402  normpar2i  28404  polid2i  28405  polidi  28406  bcsiALT  28427  lediri  28787  h1de2i  28803  cmcmlem  28841  cmbr2i  28846  cm2j  28870  fh3i  28873  fh4i  28874  pjaddii  28925  pjsslem  28929  pjssmii  28931  pjdifnormii  28933  lnopeq0lem1  29255  lnopunilem1  29260  lnophmlem2  29267  pjsdi2i  29407  pjclem1  29445  golem1  29521  dpmul100  29987  dpmul1000  29989  dpadd2  30000  dpadd  30001  dpadd3  30002  dpmul  30003  dpmul4  30004  gsumle  30161  rmulccn  30356  raddcn  30357  xrmulc1cn  30358  xrge0iifhmeo  30364  qqh0  30410  qqh1  30411  elmbfmvol2  30711  mbfmcnt  30712  eulerpartlemgvv  30820  eulerpartlemgh  30822  fib2  30847  fib3  30848  fib4  30849  fib5  30850  fib6  30851  ballotlem2  30933  ballotlemfval0  30940  ballotth  30982  hgt750lem2  31113  problem2  31938  problem4  31940  quad3  31942  pigt3  33758  poimirlem30  33795  iblabsnclem  33828  dalem10  35561  cdleme0e  36105  cdleme7c  36133  cdleme20c  36199  sqmid3api  37853  mzpcompact2lem  37924  pellexlem5  38007  pellfundgt1  38057  jm2.27c  38183  areaquad  38410  lhe4.4ex1a  39134  mccl  40400  dvnprodlem2  40732  itgsin0pilem1  40735  stoweidlem13  40799  wallispilem4  40854  wallispi2lem1  40857  wallispi2lem2  40858  dirkerper  40882  dirkertrigeqlem1  40884  fourierdlem30  40923  fourierdlem47  40939  fourierdlem103  40995  fourierdlem104  40996  fouriersw  41017  etransclem37  41057  sge0splitmpt  41197  sge0xaddlem2  41220  sge0xadd  41221  caragen0  41292  caragenuncllem  41298  fsumsplitsndif  42009  2exp5  42115  139prmALT  42119  127prm  42123  2exp11  42125  m11nprm  42126  3exp4mod41  42141  sbgoldbo  42283  2t6m3t4e0  42727  lincsum  42819  zlmodzxzequa  42886  zlmodzxzequap  42889  zlmodzxzldeplem3  42892