Theorem oveq12 7200

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 7198	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2		oveq2 7199	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
3	1, 2	sylan9eq 2791	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543  (class class class)co 7191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194

This theorem is referenced by:  oveq12i  7203  oveq12d  7209  oveqan12d  7210  mptmpoopabovd  7830  suppofssd  7923  sprmpod  7944  oev2  8228  oa00  8265  omopthi  8364  ecopoveq  8478  ecopovtrn  8480  isfsupp  8967  cantnffval  9256  fpwwe2  10222  halfnq  10555  distrlem5pr  10606  addcmpblnr  10648  ltsrpr  10656  mulgt0sr  10684  add20  11309  msqge0  11318  recextlem2  11428  cru  11787  zaddcl  12182  qaddcl  12526  qmulcl  12528  xaddval  12778  xmulval  12780  xnn0xadd0  12802  xadddilem  12849  fzopth  13114  modval  13409  1exp  13629  m1expeven  13647  nn0opthi  13801  faclbnd  13821  faclbnd3  13823  bcn0  13841  ccatopth  14246  ccatopth2  14247  repswccat  14316  reval  14634  absval  14766  clim  15020  rlim  15021  fsumparts  15333  cpnnen  15753  dvds2add  15814  dvds2sub  15815  opoe  15887  omoe  15888  opeo  15889  omeo  15890  gcddvds  16025  gcdcl  16028  gcdeq0  16039  gcdneg  16044  gcdaddmlem  16046  gcdabsOLD  16054  bezoutlem3  16064  bezout  16066  gcddiv  16074  eucalgval2  16101  lcmabs  16125  rpmul  16179  divgcdcoprmex  16186  isprm5  16227  prmexpb  16240  rpexp  16242  nn0gcdsq  16271  pcqmul  16369  prmreclem3  16434  mul4sq  16470  vdwapval  16489  f1ocpbl  16984  homfval  17149  comfval  17157  issect  17212  isfull  17371  isfth  17375  natfval  17407  catchom  17563  catcco  17565  funcsetcestrclem5  17620  plusfval  18075  0subm  18198  cycsubm  18563  cyccom  18564  isgim  18620  subgga  18648  cayleylem1  18758  lsmsubm  18996  subgdisjb  19037  pj1fval  19038  odadd1  19187  qusabl  19204  cygablOLD  19230  dprdsubg  19365  ringadd2  19547  dfrhm2  19691  isrhm  19695  isrim0  19697  scafval  19872  rmodislmodlem  19920  rmodislmod  19921  lss1d  19954  islmhm  20018  islmim  20053  znfld  20479  cygznlem3  20488  cnmsgnsubg  20493  psgnghm  20496  ipeq0  20554  ipfval  20565  dsmmval  20650  dsmmacl  20657  mplval  20907  mplcoe5lem  20950  opsrval  20957  evlval  21009  mpfind  21021  selvffval  21030  mhpfval  21033  mhpmulcl  21043  mat1dimcrng  21328  dmatval  21343  dmatmulcl  21351  scmatval  21355  scmataddcl  21367  scmatsubcl  21368  scmatmulcl  21369  mavmul0g  21404  marrepfval  21411  marrepeval  21414  marepvfval  21416  marepveval  21419  submafval  21430  submaeval  21433  mdetfval  21437  madugsum  21494  minmar1fval  21497  minmar1eval  21500  symgmatr01  21505  gsummatr01lem3  21508  gsummatr01lem4  21509  gsummatr01  21510  cpmatacl  21567  mat2pmatfval  21574  mat2pmatvalel  21576  mat2pmatmul  21582  cpm2mfval  21600  cpm2mvalel  21602  m2cpminvid  21604  m2cpminvid2  21606  decpmate  21617  pmatcollpw1  21627  monmatcollpw  21630  pmatcollpwlem  21631  pmatcollpw  21632  pmatcollpwscmatlem2  21641  pm2mpval  21646  pm2mpf1  21650  mp2pm2mplem3  21659  mp2pm2mplem4  21660  chpmatfval  21681  tx2ndc  22502  cnmpt2t  22524  cnmpt22f  22526  hmeofval  22609  qustgplem  22972  stdbdmetval  23366  nmofval  23566  nghmfval  23574  isnmhm  23598  xrsxmet  23660  isphtpy  23832  isphtpc  23845  pcorevlem  23877  cphnm  24044  tcphnmval  24080  ipcau2  24085  tcphcphlem1  24086  tcphcphlem2  24087  tcphcph  24088  bcthlem1  24175  bcth  24180  dyadmax  24449  volcn  24457  vitalilem1  24459  vitalilem2  24460  vitalilem3  24461  vitali  24464  i1fmullem  24545  itg1addlem4  24550  itg1addlem4OLD  24551  dvlip  24844  ftc1a  24888  mdegfval  24914  r1pval  25008  coeaddlem  25097  quotval  25139  elqaalem2  25167  taylfval  25205  cxpcn3  25588  resqrtcn  25589  sqrtcn  25590  abscxpbnd  25593  angval  25638  chordthmlem  25669  dcubic  25683  lgsdchr  26190  mul2sq  26254  ostthlem2  26463  tglngval  26596  islnopp  26784  ishpg  26804  finsumvtxdg2size  27592  wspthsn  27886  wwlksnon  27889  wspthsnon  27890  iswspthsnon  27894  2clwwlk  28384  numclwlk1lem2  28407  numclwwlkovh0  28409  hmoval  28845  htth  28953  normval  29159  hlimi  29223  hsn0elch  29283  ocsh  29318  shscli  29352  shs00i  29485  chj00i  29522  riesz4i  30098  stm1addi  30280  stm1add3i  30282  superpos  30389  prmidlc  31292  idlsrgmulrval  31322  brfinext  31396  submateq  31427  metidv  31510  rmulccn  31546  pl1cn  31573  sibfof  31973  cxpcncf1  32241  subfacval2  32816  txsconnlem  32869  iscvm  32888  prv  33057  bj-bary1  35166  ismblfin  35504  itg2addnclem3  35516  itg2addnc  35517  ftc1anclem3  35538  ftc1anc  35544  bfp  35668  rngo2  35751  rngohomco  35818  rngoisoval  35821  rngoisocnv  35825  crngohomfo  35850  keridl  35876  ispridlc  35914  snatpsubN  37450  cdlemn11pre  38910  dihord2pre  38925  baerlem3lem1  39407  nn0rppwr  39982  sn-inelr  40084  mendval  40652  mendplusg  40655  mulvval  41700  climf  42781  climf2  42825  cxpcncf2  43058  smflimlem3  43923  fzoopth  44435  fmtnofac2lem  44636  prmdvdsfmtnof1lem2  44653  opoeALTV  44751  opeoALTV  44752  rnghmval  45065  isrngisom  45070  rhmval  45093  rngchomALTV  45159  funcrngcsetcALT  45173  funcringcsetcALTV2lem5  45214  ringchomALTV  45222  funcringcsetclem5ALTV  45237  srhmsubclem3  45249  srhmsubc  45250  fldhmsubc  45258  srhmsubcALTVlem2  45267  srhmsubcALTV  45268  fldhmsubcALTV  45276  dmatALTval  45357  lincsumcl  45388  fdivval  45501  catprslem  45907  catprsc  45910  catprsc2  45911  thincmoALT  45927  functhinclem2  45939  fullthinc2  45944