Theorem oveq12 7418

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  (class class class)co 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  oveq12i  7421  oveq12d  7427  oveqan12d  7428  mptmpoopabovd  8068  mptmpoopabovdOLD  8070  suppofssd  8188  sprmpod  8209  oev2  8523  oa00  8559  omopthi  8660  ecopoveq  8812  ecopovtrn  8814  isfsupp  9365  cantnffval  9658  ttrcltr  9711  fpwwe2  10638  halfnq  10971  distrlem5pr  11022  addcmpblnr  11064  ltsrpr  11072  mulgt0sr  11100  add20  11726  msqge0  11735  recextlem2  11845  cru  12204  zaddcl  12602  qaddcl  12949  qmulcl  12951  xaddval  13202  xmulval  13204  xnn0xadd0  13226  xadddilem  13273  fzopth  13538  modval  13836  1exp  14057  m1expeven  14075  nn0opthi  14230  faclbnd  14250  faclbnd3  14252  bcn0  14270  ccatopth  14666  ccatopth2  14667  repswccat  14736  reval  15053  absval  15185  clim  15438  rlim  15439  fsumparts  15752  cpnnen  16172  dvds2add  16233  dvds2sub  16234  opoe  16306  omoe  16307  opeo  16308  omeo  16309  gcddvds  16444  gcdcl  16447  gcdeq0  16458  gcdneg  16463  gcdaddmlem  16465  gcdabsOLD  16473  bezoutlem3  16483  bezout  16485  gcddiv  16493  eucalgval2  16518  lcmabs  16542  rpmul  16596  divgcdcoprmex  16603  isprm5  16644  prmexpb  16657  rpexp  16659  nn0gcdsq  16688  pcqmul  16786  prmreclem3  16851  mul4sq  16887  vdwapval  16906  f1ocpbl  17471  homfval  17636  comfval  17644  issect  17700  isfull  17861  isfth  17865  natfval  17897  catchom  18053  catcco  18055  funcsetcestrclem5  18111  plusfval  18568  0subm  18698  cycsubm  19079  cyccom  19080  isgim  19136  subgga  19164  cayleylem1  19280  lsmsubm  19521  subgdisjb  19561  pj1fval  19562  odadd1  19716  qusabl  19733  imasabl  19744  dprdsubg  19894  dfrhm2  20253  isrhm  20257  isrim0OLD  20259  isrim0  20261  scafval  20491  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  lss1d  20574  islmhm  20638  islmim  20673  znfld  21116  cygznlem3  21125  cnmsgnsubg  21130  psgnghm  21133  ipeq0  21191  ipfval  21202  dsmmval  21289  dsmmacl  21296  mplval  21548  mplcoe5lem  21594  opsrval  21601  evlval  21658  mpfind  21670  selvffval  21679  mhpfval  21682  mhpmulcl  21692  mat1dimcrng  21979  dmatval  21994  dmatmulcl  22002  scmatval  22006  scmataddcl  22018  scmatsubcl  22019  scmatmulcl  22020  mavmul0g  22055  marrepfval  22062  marrepeval  22065  marepvfval  22067  marepveval  22070  submafval  22081  submaeval  22084  mdetfval  22088  madugsum  22145  minmar1fval  22148  minmar1eval  22151  symgmatr01  22156  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  cpmatacl  22218  mat2pmatfval  22225  mat2pmatvalel  22227  mat2pmatmul  22233  cpm2mfval  22251  cpm2mvalel  22253  m2cpminvid  22255  m2cpminvid2  22257  decpmate  22268  pmatcollpw1  22278  monmatcollpw  22281  pmatcollpwlem  22282  pmatcollpw  22283  pmatcollpwscmatlem2  22292  pm2mpval  22297  pm2mpf1  22301  mp2pm2mplem3  22310  mp2pm2mplem4  22311  chpmatfval  22332  tx2ndc  23155  cnmpt2t  23177  cnmpt22f  23179  hmeofval  23262  qustgplem  23625  stdbdmetval  24023  nmofval  24231  nghmfval  24239  isnmhm  24263  xrsxmet  24325  isphtpy  24497  isphtpc  24510  pcorevlem  24542  cphnm  24710  tcphnmval  24746  ipcau2  24751  tcphcphlem1  24752  tcphcphlem2  24753  tcphcph  24754  bcthlem1  24841  bcth  24846  dyadmax  25115  volcn  25123  vitalilem1  25125  vitalilem2  25126  vitalilem3  25127  vitali  25130  i1fmullem  25211  itg1addlem4  25216  itg1addlem4OLD  25217  dvlip  25510  ftc1a  25554  mdegfval  25580  r1pval  25674  coeaddlem  25763  quotval  25805  elqaalem2  25833  taylfval  25871  cxpcn3  26256  resqrtcn  26257  sqrtcn  26258  abscxpbnd  26261  angval  26306  chordthmlem  26337  dcubic  26351  lgsdchr  26858  mul2sq  26922  ostthlem2  27131  tglngval  27833  islnopp  28021  ishpg  28041  finsumvtxdg2size  28838  wspthsn  29133  wwlksnon  29136  wspthsnon  29137  iswspthsnon  29141  2clwwlk  29631  numclwlk1lem2  29654  numclwwlkovh0  29656  hmoval  30094  htth  30202  normval  30408  hlimi  30472  hsn0elch  30532  ocsh  30567  shscli  30601  shs00i  30734  chj00i  30771  riesz4i  31347  stm1addi  31529  stm1add3i  31531  superpos  31638  prmidlc  32598  idlsrgmulrval  32654  brfinext  32763  irngval  32780  minplyval  32797  submateq  32820  metidv  32903  rmulccn  32939  pl1cn  32966  sibfof  33370  cxpcncf1  33638  subfacval2  34209  txsconnlem  34262  iscvm  34281  prv  34450  ovmul  35191  gg-divcn  35194  gg-divccn  35196  gg-iihalf1cn  35198  gg-iihalf2cn  35199  gg-icchmeo  35201  gg-cnrehmeo  35202  gg-reparphti  35203  gg-mulcncf  35204  gg-plycn  35208  gg-psercn2  35209  gg-rmulccn  35210  gg-cxpcn  35215  bj-bary1  36241  ismblfin  36577  itg2addnclem3  36589  itg2addnc  36590  ftc1anclem3  36611  ftc1anc  36617  bfp  36740  rngo2  36823  rngohomco  36890  rngoisoval  36893  rngoisocnv  36897  crngohomfo  36922  keridl  36948  ispridlc  36986  snatpsubN  38669  cdlemn11pre  40129  dihord2pre  40144  baerlem3lem1  40626  nn0rppwr  41272  sn-inelr  41386  prjcrvfval  41421  mendval  41973  mendplusg  41976  omcl3g  42132  mulvval  43275  climf  44386  climf2  44430  cxpcncf2  44663  smflimlem3  45537  fzoopth  46083  fmtnofac2lem  46284  prmdvdsfmtnof1lem2  46301  opoeALTV  46399  opeoALTV  46400  rnghmval  46737  isrngisom  46742  rhmval  46770  pzriprnglem5  46857  pzriprnglem8  46860  rngchomALTV  46931  funcrngcsetcALT  46945  funcringcsetcALTV2lem5  46986  ringchomALTV  46994  funcringcsetclem5ALTV  47009  srhmsubclem3  47021  srhmsubc  47022  fldhmsubc  47030  srhmsubcALTVlem2  47039  srhmsubcALTV  47040  fldhmsubcALTV  47048  dmatALTval  47129  lincsumcl  47160  fdivval  47273  catprslem  47678  catprsc  47681  catprsc2  47682  thincmoALT  47698  functhinclem2  47710  fullthinc2  47715