Theorem oveq12i 7460

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

Syntax hints:   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  oveq123i  7462  caovdir  7684  caovdilem  7685  caovlem2  7686  cnfcom2  9771  canthwelem  10719  adderpqlem  11023  addassnq  11027  distrnq  11030  ltanq  11040  1lt2nq  11042  ltexnq  11044  halfnq  11045  mulcmpblnrlem  11139  mulcomsr  11158  distrsr  11160  m1p1sr  11161  m1m1sr  11162  mulgt0sr  11174  addcnsrec  11212  mulcnsrec  11213  axmulcom  11224  axmulass  11226  axdistr  11227  axi2m1  11228  addrid  11470  3t3e9  12460  8th4div3  12513  halfpm6th  12514  numma  12802  decmul10add  12827  4t3lem  12855  9t11e99  12888  halfthird  12901  5recm6rec  12902  fz0to3un2pr  13686  seqfeq4  14102  seqof  14110  sqdivi  14234  sq4e2t8  14248  i4  14253  binom2i  14261  nn0opthlem1  14317  facp1  14327  fac2  14328  fac3  14329  fac4  14330  faclbnd4lem1  14342  4bc2eq6  14378  ccat2s1len  14671  ccat2s1p2  14678  cats1len  14909  cats2cat  14911  ofs2  15020  cji  15208  01sqrexlem5  15295  fsumadd  15788  fsumsplitf  15790  fsumsplitsnun  15803  0.999...  15929  fprodmul  16008  fproddiv  16009  fprodsplitf  16036  bpoly3  16106  fsumcube  16108  efsep  16158  ef01bndlem  16232  cos2bnd  16236  rpnnen2lem3  16264  3dvds2dec  16381  flodddiv4  16461  sadeq  16518  gcdaddmlem  16570  bezout  16590  nn0expgcd  16611  nn0gcdsq  16799  pythagtriplem16  16877  4sqlem19  17010  dec5nprm  17113  dec2nprm  17114  mod2xnegi  17118  numexp2x  17126  decsplit  17130  karatsuba  17131  2exp5  17133  2exp11  17137  2exp16  17138  37prm  17168  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  funcoppc  17939  estrchom  18195  funcestrcsetclem5  18213  yonedalem3b  18349  ecqusaddd  19232  symgressbas  19423  gsum2dlem2  20013  opprrng  20371  isrhm  20504  rngqiprnglinlem2  21325  pzriprng1ALT  21530  evlsval  22133  mamudi  22428  mamudir  22429  oftpos  22479  mamutpos  22485  mdetrlin  22629  mdetrlin2  22634  mdetunilem5  22643  cpmadugsumfi  22904  cnmpt2res  23706  ussval  24289  icopnfhmeo  24993  iccpnfhmeo  24995  pcoass  25076  ovolunlem1a  25550  ioombl1lem3  25614  ioombl1lem4  25615  mbfimaopnlem  25709  itgfsum  25882  iblabslem  25883  itgsplit  25891  dveflem  26037  efhalfpi  26531  efipi  26533  sin2pi  26535  ef2pi  26537  sincosq3sgn  26560  sincosq4sgn  26561  sinq34lt0t  26569  sincos4thpi  26573  tan4thpi  26574  tan4thpiOLD  26575  sincos6thpi  26576  sincos3rdpi  26577  pigt3  26578  pige3ALT  26580  cxpcn3  26809  lawcos  26877  1cubrlem  26902  quart1lem  26916  quart1  26917  asin1  26955  atancj  26971  atanlogsublem  26976  log2cnv  27005  log2tlbnd  27006  log2ublem3  27009  log2ub  27010  birthday  27015  basellem8  27149  basellem9  27150  cht2  27233  cht3  27234  1sgm2ppw  27262  bclbnd  27342  bposlem8  27353  bposlem9  27354  lgsdi  27396  lgsquadlem1  27442  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  addsqnreup  27505  addsval2  28014  addsunif  28053  addsasslem1  28054  addsasslem2  28055  negsval  28075  negs0s  28076  negs1s  28077  negsid  28091  mulsval2  28155  muls01  28156  mulsproplem2  28161  mulsproplem3  28162  mulsproplem4  28163  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  mulsunif  28194  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  mulsunif2  28214  precsexlem11  28259  onmulscl  28305  1p1e2s  28418  nohalf  28425  0reno  28447  mirauto  28710  axsegconlem9  28958  ax5seglem7  28968  vtxdginducedm1  29579  clwlkclwwlkfo  30041  eupth2eucrct  30249  ex-exp  30482  ex-fac  30483  ex-bc  30484  ex-hash  30485  ip0i  30857  ip1ilem  30858  ip2i  30860  ipdirilem  30861  ipasslem10  30871  ip2dii  30876  pythi  30882  siilem1  30883  hvsubsub4i  31091  hvsubcan2i  31096  hisubcomi  31136  normlem0  31141  normlem1  31142  normlem2  31143  normlem3  31144  normlem6  31147  normlem8  31149  normlem9  31150  bcseqi  31152  norm-ii-i  31169  norm-iii-i  31171  normpythi  31174  norm3difi  31179  normpari  31186  normpar2i  31188  polid2i  31189  polidi  31190  bcsiALT  31211  lediri  31569  h1de2i  31585  cmcmlem  31623  cmbr2i  31628  cm2j  31652  fh3i  31655  fh4i  31656  pjaddii  31707  pjsslem  31711  pjssmii  31713  pjdifnormii  31715  lnopeq0lem1  32037  lnopunilem1  32042  lnophmlem2  32049  pjsdi2i  32189  pjclem1  32227  golem1  32303  dpmul100  32861  dpmul1000  32863  dpadd2  32874  dpadd  32875  dpadd3  32876  dpmul  32877  dpmul4  32878  ccatws1f1o  32918  gsumle  33074  matdim  33628  rmulccn  33874  raddcn  33875  xrmulc1cn  33876  xrge0iifhmeo  33882  qqh0  33930  qqh1  33931  elmbfmvol2  34232  mbfmcnt  34233  eulerpartlemgvv  34341  eulerpartlemgh  34343  fib2  34367  fib3  34368  fib4  34369  fib5  34370  fib6  34371  ballotlem2  34453  ballotlemfval0  34460  ballotth  34502  hgt750lem2  34629  problem2  35634  problem4  35636  quad3  35638  ditgeq123i  36173  cbvditgvw2  36215  poimirlem30  37610  iblabsnclem  37643  dalem10  39630  cdleme0e  40174  cdleme7c  40202  cdleme20c  40268  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1  42033  5bc2eq10  42099  aks5lem3a  42146  sn-1ne2  42254  sqmid3api  42272  sqdeccom12  42278  sq3deccom12  42279  tan3rdpi  42338  rei4  42399  ipiiie0  42413  sn-0tie0  42415  mzpcompact2lem  42707  pellexlem5  42789  pellfundgt1  42839  jm2.27c  42964  areaquad  43177  resqrtvalex  43607  imsqrtvalex  43608  lhe4.4ex1a  44298  mccl  45519  dvnprodlem2  45868  itgsin0pilem1  45871  stoweidlem13  45934  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  dirkerper  46017  dirkertrigeqlem1  46019  fourierdlem30  46058  fourierdlem47  46074  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  etransclem37  46192  sge0splitmpt  46332  sge0xaddlem2  46355  sge0xadd  46356  caragen0  46427  caragenuncllem  46433  fsumsplitsndif  47247  139prmALT  47470  127prm  47473  m11nprm  47475  3exp4mod41  47490  sbgoldbo  47661  2t6m3t4e0  48073  lincsum  48158  zlmodzxzequa  48225  zlmodzxzequap  48228  zlmodzxzldeplem3  48231  rrx2linest  48476  line2  48486  itsclc0yqsollem1  48496  itsclquadb  48510  itscnhlinecirc02plem2  48517