Theorem oveq12 7264

Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)

Assertion

Ref	Expression
oveq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12

Step	Hyp	Ref	Expression
1		oveq1 7262	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2		oveq2 7263	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
3	1, 2	sylan9eq 2799	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  oveq12i  7267  oveq12d  7273  oveqan12d  7274  mptmpoopabovd  7895  suppofssd  7990  sprmpod  8011  oev2  8315  oa00  8352  omopthi  8451  ecopoveq  8565  ecopovtrn  8567  isfsupp  9062  cantnffval  9351  fpwwe2  10330  halfnq  10663  distrlem5pr  10714  addcmpblnr  10756  ltsrpr  10764  mulgt0sr  10792  add20  11417  msqge0  11426  recextlem2  11536  cru  11895  zaddcl  12290  qaddcl  12634  qmulcl  12636  xaddval  12886  xmulval  12888  xnn0xadd0  12910  xadddilem  12957  fzopth  13222  modval  13519  1exp  13740  m1expeven  13758  nn0opthi  13912  faclbnd  13932  faclbnd3  13934  bcn0  13952  ccatopth  14357  ccatopth2  14358  repswccat  14427  reval  14745  absval  14877  clim  15131  rlim  15132  fsumparts  15446  cpnnen  15866  dvds2add  15927  dvds2sub  15928  opoe  16000  omoe  16001  opeo  16002  omeo  16003  gcddvds  16138  gcdcl  16141  gcdeq0  16152  gcdneg  16157  gcdaddmlem  16159  gcdabsOLD  16167  bezoutlem3  16177  bezout  16179  gcddiv  16187  eucalgval2  16214  lcmabs  16238  rpmul  16292  divgcdcoprmex  16299  isprm5  16340  prmexpb  16353  rpexp  16355  nn0gcdsq  16384  pcqmul  16482  prmreclem3  16547  mul4sq  16583  vdwapval  16602  f1ocpbl  17153  homfval  17318  comfval  17326  issect  17382  isfull  17542  isfth  17546  natfval  17578  catchom  17734  catcco  17736  funcsetcestrclem5  17792  plusfval  18248  0subm  18371  cycsubm  18736  cyccom  18737  isgim  18793  subgga  18821  cayleylem1  18935  lsmsubm  19173  subgdisjb  19214  pj1fval  19215  odadd1  19364  qusabl  19381  cygablOLD  19407  dprdsubg  19542  ringadd2  19729  dfrhm2  19876  isrhm  19880  isrim0  19882  scafval  20057  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  lss1d  20140  islmhm  20204  islmim  20239  znfld  20680  cygznlem3  20689  cnmsgnsubg  20694  psgnghm  20697  ipeq0  20755  ipfval  20766  dsmmval  20851  dsmmacl  20858  mplval  21107  mplcoe5lem  21150  opsrval  21157  evlval  21215  mpfind  21227  selvffval  21236  mhpfval  21239  mhpmulcl  21249  mat1dimcrng  21534  dmatval  21549  dmatmulcl  21557  scmatval  21561  scmataddcl  21573  scmatsubcl  21574  scmatmulcl  21575  mavmul0g  21610  marrepfval  21617  marrepeval  21620  marepvfval  21622  marepveval  21625  submafval  21636  submaeval  21639  mdetfval  21643  madugsum  21700  minmar1fval  21703  minmar1eval  21706  symgmatr01  21711  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  cpmatacl  21773  mat2pmatfval  21780  mat2pmatvalel  21782  mat2pmatmul  21788  cpm2mfval  21806  cpm2mvalel  21808  m2cpminvid  21810  m2cpminvid2  21812  decpmate  21823  pmatcollpw1  21833  monmatcollpw  21836  pmatcollpwlem  21837  pmatcollpw  21838  pmatcollpwscmatlem2  21847  pm2mpval  21852  pm2mpf1  21856  mp2pm2mplem3  21865  mp2pm2mplem4  21866  chpmatfval  21887  tx2ndc  22710  cnmpt2t  22732  cnmpt22f  22734  hmeofval  22817  qustgplem  23180  stdbdmetval  23576  nmofval  23784  nghmfval  23792  isnmhm  23816  xrsxmet  23878  isphtpy  24050  isphtpc  24063  pcorevlem  24095  cphnm  24262  tcphnmval  24298  ipcau2  24303  tcphcphlem1  24304  tcphcphlem2  24305  tcphcph  24306  bcthlem1  24393  bcth  24398  dyadmax  24667  volcn  24675  vitalilem1  24677  vitalilem2  24678  vitalilem3  24679  vitali  24682  i1fmullem  24763  itg1addlem4  24768  itg1addlem4OLD  24769  dvlip  25062  ftc1a  25106  mdegfval  25132  r1pval  25226  coeaddlem  25315  quotval  25357  elqaalem2  25385  taylfval  25423  cxpcn3  25806  resqrtcn  25807  sqrtcn  25808  abscxpbnd  25811  angval  25856  chordthmlem  25887  dcubic  25901  lgsdchr  26408  mul2sq  26472  ostthlem2  26681  tglngval  26816  islnopp  27004  ishpg  27024  finsumvtxdg2size  27820  wspthsn  28114  wwlksnon  28117  wspthsnon  28118  iswspthsnon  28122  2clwwlk  28612  numclwlk1lem2  28635  numclwwlkovh0  28637  hmoval  29073  htth  29181  normval  29387  hlimi  29451  hsn0elch  29511  ocsh  29546  shscli  29580  shs00i  29713  chj00i  29750  riesz4i  30326  stm1addi  30508  stm1add3i  30510  superpos  30617  prmidlc  31526  idlsrgmulrval  31556  brfinext  31630  submateq  31661  metidv  31744  rmulccn  31780  pl1cn  31807  sibfof  32207  cxpcncf1  32475  subfacval2  33049  txsconnlem  33102  iscvm  33121  prv  33290  ttrcltr  33702  bj-bary1  35410  ismblfin  35745  itg2addnclem3  35757  itg2addnc  35758  ftc1anclem3  35779  ftc1anc  35785  bfp  35909  rngo2  35992  rngohomco  36059  rngoisoval  36062  rngoisocnv  36066  crngohomfo  36091  keridl  36117  ispridlc  36155  snatpsubN  37691  cdlemn11pre  39151  dihord2pre  39166  baerlem3lem1  39648  nn0rppwr  40254  sn-inelr  40356  mendval  40924  mendplusg  40927  mulvval  41975  climf  43053  climf2  43097  cxpcncf2  43330  smflimlem3  44195  fzoopth  44707  fmtnofac2lem  44908  prmdvdsfmtnof1lem2  44925  opoeALTV  45023  opeoALTV  45024  rnghmval  45337  isrngisom  45342  rhmval  45365  rngchomALTV  45431  funcrngcsetcALT  45445  funcringcsetcALTV2lem5  45486  ringchomALTV  45494  funcringcsetclem5ALTV  45509  srhmsubclem3  45521  srhmsubc  45522  fldhmsubc  45530  srhmsubcALTVlem2  45539  srhmsubcALTV  45540  fldhmsubcALTV  45548  dmatALTval  45629  lincsumcl  45660  fdivval  45773  catprslem  46179  catprsc  46182  catprsc2  46183  thincmoALT  46199  functhinclem2  46211  fullthinc2  46216