Theorem oveq12i 6561

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 6558	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	mp2an 704	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Syntax hints:   = 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:  oveq123i  6563  caovdir  6766  caovdilem  6767  caovlem2  6768  cnfcom2  8482  canthwelem  9351  adderpqlem  9655  addassnq  9659  distrnq  9662  ltanq  9672  1lt2nq  9674  ltexnq  9676  halfnq  9677  mulcmpblnrlem  9770  mulcomsr  9789  distrsr  9791  m1p1sr  9792  m1m1sr  9793  mulgt0sr  9805  addcnsrec  9843  mulcnsrec  9844  axmulcom  9855  axmulass  9857  axdistr  9858  axi2m1  9859  addid1  10095  3t3e9  11057  8th4div3  11129  halfpm6th  11130  numma  11433  decmul10add  11469  decmul10addOLD  11470  4t3lem  11507  9t11e99  11547  9t11e99OLD  11548  halfthird  11561  5recm6rec  11562  fz0to3un2pr  12310  seqfeq4  12712  seqof  12720  sqdivi  12810  sq4e2t8  12824  i4  12829  binom2i  12836  nn0opthlem1  12917  facp1  12927  fac2  12928  fac3  12929  fac4  12930  faclbnd4lem1  12942  4bc2eq6  12978  ccat2s1len  13253  ccat2s1p2  13258  cats1len  13456  cats2cat  13458  ofs2  13558  cji  13747  sqrlem5  13835  fsumadd  14317  fsumsplitsnun  14328  0.999...  14451  0.999...OLD  14452  fprodmul  14529  fproddiv  14530  fprodsplitf  14558  bpoly3  14628  fsumcube  14630  efsep  14679  ef01bndlem  14753  cos2bnd  14757  rpnnen2lem3  14784  3dvds2dec  14894  3dvds2decOLD  14895  flodddiv4  14975  sadeq  15032  gcdaddmlem  15083  bezout  15098  nn0gcdsq  15298  pythagtriplem16  15373  4sqlem19  15505  dec5nprm  15608  dec2nprm  15609  mod2xnegi  15613  numexp2x  15621  decsplit  15625  decsplitOLD  15629  karatsuba  15630  karatsubaOLD  15631  2exp16  15635  37prm  15666  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  funcoppc  16358  estrchom  16590  funcestrcsetclem5  16607  yonedalem3b  16742  gsum2dlem2  18193  opprring  18454  isrhm  18544  evlsval  19340  mamudi  20028  mamudir  20029  oftpos  20077  mamutpos  20083  mdetrlin  20227  mdetrlin2  20232  mdetunilem5  20241  cpmadugsumfi  20501  cnmpt2res  21290  ussval  21873  icopnfhmeo  22550  iccpnfhmeo  22552  pcoass  22632  ovolunlem1a  23071  ioombl1lem3  23135  ioombl1lem4  23136  mbfimaopnlem  23228  iblcnlem1  23360  itgfsum  23399  iblabslem  23400  itgsplit  23408  dveflem  23546  efhalfpi  24027  efipi  24029  sin2pi  24031  ef2pi  24033  sincosq3sgn  24056  sincosq4sgn  24057  sinq34lt0t  24065  sincos4thpi  24069  tan4thpi  24070  sincos6thpi  24071  sincos3rdpi  24072  pige3  24073  cxpcn3  24289  lawcos  24346  1cubrlem  24368  quart1lem  24382  quart1  24383  asin1  24421  atancj  24437  atanlogsublem  24442  log2cnv  24471  log2tlbnd  24472  log2ublem3  24475  log2ub  24476  birthday  24481  basellem8  24614  basellem9  24615  cht2  24698  cht3  24699  1sgm2ppw  24725  bclbnd  24805  bposlem8  24816  bposlem9  24817  lgsdi  24859  lgsquadlem1  24905  2lgsoddprmlem3c  24937  2lgsoddprmlem3d  24938  mirauto  25379  axsegconlem9  25605  ax5seglem7  25615  clwlkfoclwwlk  26372  vdgr0  26427  vdegp1bi  26512  ex-exp  26699  ex-fac  26700  ex-bc  26701  ex-hash  26702  ip0i  27064  ip1ilem  27065  ip2i  27067  ipdirilem  27068  ipasslem10  27078  ip2dii  27083  pythi  27089  siilem1  27090  hvsubsub4i  27300  hvsubcan2i  27305  hisubcomi  27345  normlem0  27350  normlem1  27351  normlem2  27352  normlem3  27353  normlem6  27356  normlem8  27358  normlem9  27359  bcseqi  27361  norm-ii-i  27378  norm-iii-i  27380  normpythi  27383  norm3difi  27388  normpari  27395  normpar2i  27397  polid2i  27398  polidi  27399  bcsiALT  27420  lediri  27780  h1de2i  27796  cmcmlem  27834  cmbr2i  27839  cm2j  27863  fh3i  27866  fh4i  27867  pjaddii  27918  pjsslem  27922  pjssmii  27924  pjdifnormii  27926  lnopeq0lem1  28248  lnopunilem1  28253  lnophmlem2  28260  pjsdi2i  28400  pjclem1  28438  golem1  28514  gsumle  29110  rmulccn  29302  raddcn  29303  xrmulc1cn  29304  xrge0iifhmeo  29310  qqh0  29356  qqh1  29357  elmbfmvol2  29656  mbfmcnt  29657  eulerpartlemgvv  29765  eulerpartlemgh  29767  fib2  29791  fib3  29792  fib4  29793  fib5  29794  fib6  29795  ballotlem2  29877  ballotlemfval0  29884  ballotth  29926  problem2  30813  problem2OLD  30814  problem4  30816  quad3  30818  pigt3  32572  poimirlem30  32609  iblabsnclem  32643  dalem10  33977  cdleme0e  34522  cdleme7c  34550  cdleme20c  34617  mzpcompact2lem  36332  pellexlem5  36415  pellfundgt1  36465  jm2.27c  36592  areaquad  36821  lhe4.4ex1a  37550  fsumsplitf  38634  mccl  38665  dvnprodlem2  38837  itgsin0pilem1  38841  stoweidlem13  38906  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  dirkerper  38989  dirkertrigeqlem1  38991  fourierdlem30  39030  fourierdlem47  39046  fourierdlem103  39102  fourierdlem104  39103  fouriersw  39124  etransclem37  39164  sge0splitmpt  39304  sge0xaddlem2  39327  sge0xadd  39328  caragen0  39396  caragenuncllem  39402  2exp5  40045  139prmALT  40049  127prm  40053  2exp11  40055  m11nprm  40056  3exp4mod41  40071  fsumsplitsndif  40372  clwlksfoclwwlk  41270  eupth2eucrct  41385  2t6m3t4e0  41919  lincsum  42012  zlmodzxzequa  42079  zlmodzxzequap  42082  zlmodzxzldeplem3  42085