Theorem oveq12i 6662

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	|- A = B
oveq12i.2	|- C = D

Assertion

Ref	Expression
oveq12i	|- ( A F C ) = ( B F D )

Proof of Theorem oveq12i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq12i.2	. 2 |- C = D
3		oveq12 6659	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	mp2an 708	1 |- ( A F C ) = ( B F D )

Syntax hints:   = wceq 1483  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  oveq123i  6664  caovdir  6868  caovdilem  6869  caovlem2  6870  cnfcom2  8599  canthwelem  9472  adderpqlem  9776  addassnq  9780  distrnq  9783  ltanq  9793  1lt2nq  9795  ltexnq  9797  halfnq  9798  mulcmpblnrlem  9891  mulcomsr  9910  distrsr  9912  m1p1sr  9913  m1m1sr  9914  mulgt0sr  9926  addcnsrec  9964  mulcnsrec  9965  axmulcom  9976  axmulass  9978  axdistr  9979  axi2m1  9980  addid1  10216  3t3e9  11180  8th4div3  11252  halfpm6th  11253  numma  11557  decmul10add  11593  decmul10addOLD  11594  4t3lem  11631  9t11e99  11671  9t11e99OLD  11672  halfthird  11685  5recm6rec  11686  fz0to3un2pr  12441  seqfeq4  12850  seqof  12858  sqdivi  12948  sq4e2t8  12962  i4  12967  binom2i  12974  nn0opthlem1  13055  facp1  13065  fac2  13066  fac3  13067  fac4  13068  faclbnd4lem1  13080  4bc2eq6  13116  ccat2s1len  13400  ccat2s1p2  13406  cats1len  13605  cats2cat  13607  ofs2  13710  cji  13899  sqrlem5  13987  fsumadd  14470  fsumsplitf  14472  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  0.999...  14612  0.999...OLD  14613  fprodmul  14690  fproddiv  14691  fprodsplitf  14719  bpoly3  14789  fsumcube  14791  efsep  14840  ef01bndlem  14914  cos2bnd  14918  rpnnen2lem3  14945  3dvds2dec  15056  3dvds2decOLD  15057  flodddiv4  15137  sadeq  15194  gcdaddmlem  15245  bezout  15260  nn0gcdsq  15460  pythagtriplem16  15535  4sqlem19  15667  dec5nprm  15770  dec2nprm  15771  mod2xnegi  15775  numexp2x  15783  decsplit  15787  decsplitOLD  15791  karatsuba  15792  karatsubaOLD  15793  2exp16  15797  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  funcoppc  16535  estrchom  16767  funcestrcsetclem5  16784  yonedalem3b  16919  gsum2dlem2  18370  opprring  18631  isrhm  18721  evlsval  19519  mamudi  20209  mamudir  20210  oftpos  20258  mamutpos  20264  mdetrlin  20408  mdetrlin2  20413  mdetunilem5  20422  cpmadugsumfi  20682  cnmpt2res  21480  ussval  22063  icopnfhmeo  22742  iccpnfhmeo  22744  pcoass  22824  ovolunlem1a  23264  ioombl1lem3  23328  ioombl1lem4  23329  mbfimaopnlem  23422  iblcnlem1  23554  itgfsum  23593  iblabslem  23594  itgsplit  23602  dveflem  23742  efhalfpi  24223  efipi  24225  sin2pi  24227  ef2pi  24229  sincosq3sgn  24252  sincosq4sgn  24253  sinq34lt0t  24261  sincos4thpi  24265  tan4thpi  24266  sincos6thpi  24267  sincos3rdpi  24268  pige3  24269  cxpcn3  24489  lawcos  24546  1cubrlem  24568  quart1lem  24582  quart1  24583  asin1  24621  atancj  24637  atanlogsublem  24642  log2cnv  24671  log2tlbnd  24672  log2ublem3  24675  log2ub  24676  birthday  24681  basellem8  24814  basellem9  24815  cht2  24898  cht3  24899  1sgm2ppw  24925  bclbnd  25005  bposlem8  25016  bposlem9  25017  lgsdi  25059  lgsquadlem1  25105  2lgsoddprmlem3c  25137  2lgsoddprmlem3d  25138  mirauto  25579  axsegconlem9  25805  ax5seglem7  25815  vtxdginducedm1  26439  clwlksfoclwwlk  26963  eupth2eucrct  27077  ex-exp  27307  ex-fac  27308  ex-bc  27309  ex-hash  27310  ip0i  27680  ip1ilem  27681  ip2i  27683  ipdirilem  27684  ipasslem10  27694  ip2dii  27699  pythi  27705  siilem1  27706  hvsubsub4i  27916  hvsubcan2i  27921  hisubcomi  27961  normlem0  27966  normlem1  27967  normlem2  27968  normlem3  27969  normlem6  27972  normlem8  27974  normlem9  27975  bcseqi  27977  norm-ii-i  27994  norm-iii-i  27996  normpythi  27999  norm3difi  28004  normpari  28011  normpar2i  28013  polid2i  28014  polidi  28015  bcsiALT  28036  lediri  28396  h1de2i  28412  cmcmlem  28450  cmbr2i  28455  cm2j  28479  fh3i  28482  fh4i  28483  pjaddii  28534  pjsslem  28538  pjssmii  28540  pjdifnormii  28542  lnopeq0lem1  28864  lnopunilem1  28869  lnophmlem2  28876  pjsdi2i  29016  pjclem1  29054  golem1  29130  dpmul100  29605  dpmul1000  29607  dpadd2  29618  dpadd  29619  dpadd3  29620  dpmul  29621  dpmul4  29622  gsumle  29779  rmulccn  29974  raddcn  29975  xrmulc1cn  29976  xrge0iifhmeo  29982  qqh0  30028  qqh1  30029  elmbfmvol2  30329  mbfmcnt  30330  eulerpartlemgvv  30438  eulerpartlemgh  30440  fib2  30464  fib3  30465  fib4  30466  fib5  30467  fib6  30468  ballotlem2  30550  ballotlemfval0  30557  ballotth  30599  hgt750lem2  30730  problem2  31559  problem2OLD  31560  problem4  31562  quad3  31564  pigt3  33402  poimirlem30  33439  iblabsnclem  33473  dalem10  34959  cdleme0e  35504  cdleme7c  35532  cdleme20c  35599  mzpcompact2lem  37314  pellexlem5  37397  pellfundgt1  37447  jm2.27c  37574  areaquad  37802  lhe4.4ex1a  38528  mccl  39830  dvnprodlem2  40162  itgsin0pilem1  40165  stoweidlem13  40230  wallispilem4  40285  wallispi2lem1  40288  wallispi2lem2  40289  dirkerper  40313  dirkertrigeqlem1  40315  fourierdlem30  40354  fourierdlem47  40370  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  etransclem37  40488  sge0splitmpt  40628  sge0xaddlem2  40651  sge0xadd  40652  caragen0  40720  caragenuncllem  40726  fsumsplitsndif  41343  2exp5  41507  139prmALT  41511  127prm  41515  2exp11  41517  m11nprm  41518  3exp4mod41  41533  sbgoldbo  41675  2t6m3t4e0  42126  lincsum  42218  zlmodzxzequa  42285  zlmodzxzequap  42288  zlmodzxzldeplem3  42291