Theorem oveq12 7419

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1570  (class class class)co 7410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is used by:  oveq12i  7422  oveq12d  7428  oveqan12d  7429  ovmpot  7571  mptmpoopabovd  8075  suppofssd  8195  sprmpod  8216  oev2  8504  oa00  8540  omopthi  8643  ecopoveq  8812  ecopovtrn  8814  isfsupp  9321  cantnffval  9628  ttrcltr  9681  fpwwe2lem4  10623  fpwwe2  10632  pwfseqlem4  10651  halfnq  10965  distrlem5pr  11016  addcmpblnr  11058  ltsrpr  11066  mulgt0sr  11094  add20  11730  msqge0  11739  recextlem2  11849  cru  12214  zaddcl  12638  qaddcl  12993  qmulcl  12995  xaddval  13253  xmulval  13255  xnn0xadd0  13277  xadddilem  13324  fzopth  13594  fzoopth  13796  modval  13909  1exp  14132  m1expeven  14150  nn0opthi  14311  faclbnd  14331  faclbnd3  14333  bcn0  14351  ccatopth  14758  ccatopth2  14759  repswccat  14828  reval  15162  absval  15294  clim  15550  rlim  15551  fsumparts  15863  cpnnen  16289  dvds2add  16352  dvds2sub  16353  opoe  16425  omoe  16426  opeo  16427  omeo  16428  gcddvds  16565  gcdcl  16568  gcdeq0  16579  gcdneg  16584  gcdaddmlem  16586  bezoutlem3  16603  bezout  16605  gcddiv  16613  nn0rppwr  16623  eucalgval2  16643  lcmabs  16667  rpmul  16721  divgcdcoprmex  16728  isprm5  16770  prmexpb  16782  rpexp  16785  nn0gcdsq  16815  pcqmul  16917  prmreclem3  16982  mul4sq  17018  vdwapval  17037  f1ocpbl  17583  homfval  17752  comfval  17760  issect  17814  isfull  17973  isfth  17977  natfval  18010  catchom  18164  catcco  18166  funcsetcestrclem5  18219  plusfval  18709  0subm  18880  cycsubm  19277  cyccom  19278  isgim  19336  subgga  19374  cayleylem1  19486  lsmsubm  19727  subgdisjb  19767  pj1fval  19768  odadd1  19922  qusabl  19939  imasabl  19950  dprdsubg  20100  rnghmval  20527  isrngim  20532  dfrhm2  20561  rhmval0  20562  isrhm  20566  isrim0  20570  crngrhmfo  20583  rhmval  20595  funcrngcsetcALT  20749  srhmsubclem3  20787  srhmsubc  20788  fldhmsubc  20897  scafval  21011  rmodislmodlem  21059  rmodislmod  21060  lss1d  21093  islmhm  21157  islmim  21192  prmidlc  21482  pzriprnglem5  21644  pzriprnglem8  21647  znfld  21719  cygznlem3  21728  cnmsgnsubg  21736  psgnghm  21739  ipeq0  21797  ipfval  21808  dsmmval  21893  dsmmacl  21900  mplval  22147  mplcoe5lem  22199  opsrval  22206  evlval  22260  mpfind  22275  selvffval  22278  mhpfval  22310  mhpmulcl  22321  psdffval  22329  mat1dimcrng  22643  dmatval  22658  dmatmulcl  22666  scmatval  22670  scmataddcl  22682  scmatsubcl  22683  scmatmulcl  22684  mavmul0g  22719  marrepfval  22726  marrepeval  22729  marepvfval  22731  marepveval  22734  submafval  22745  submaeval  22748  mdetfval  22752  madugsum  22809  minmar1fval  22812  minmar1eval  22815  symgmatr01  22820  gsummatr01lem3  22823  gsummatr01lem4  22824  gsummatr01  22825  cpmatacl  22882  mat2pmatfval  22889  mat2pmatvalel  22891  mat2pmatmul  22897  cpm2mfval  22915  cpm2mvalel  22917  m2cpminvid  22919  m2cpminvid2  22921  decpmate  22932  pmatcollpw1  22942  monmatcollpw  22945  pmatcollpwlem  22946  pmatcollpw  22947  pmatcollpwscmatlem2  22956  pm2mpval  22961  pm2mpf1  22965  mp2pm2mplem3  22974  mp2pm2mplem4  22975  chpmatfval  22996  tx2ndc  23817  cnmpt2t  23839  cnmpt22f  23841  hmeofval  23924  qustgplem  24287  stdbdmetval  24680  nmofval  24880  nghmfval  24888  isnmhm  24912  xrsxmet  24976  divcn  25036  divccn  25041  iihalf1cn  25100  iihalf2cn  25102  icchmeo  25109  cnrehmeo  25121  isphtpy  25149  isphtpc  25162  reparphti  25165  pcorevlem  25194  cphnm  25361  tcphnmval  25397  ipcau2  25402  tcphcphlem1  25403  tcphcphlem2  25404  tcphcph  25405  bcthlem1  25492  bcth  25497  mulcncf  25614  dyadmax  25766  volcn  25774  vitalilem1  25776  vitalilem2  25777  vitalilem3  25778  vitali  25781  i1fmullem  25862  itg1addlem4  25867  dvlip  26161  ftc1a  26205  mdegfval  26228  r1pval  26324  coeaddlem  26415  plycn  26427  quotval  26462  elqaalem2  26490  taylfval  26531  psercn2  26595  cxpcn  26919  cxpcn3  26922  resqrtcn  26923  sqrtcn  26924  abscxpbnd  26927  angval  26975  chordthmlem  27006  dcubic  27020  efrlim  27143  lgsdchr  27528  mul2sq  27592  ostthlem2  27801  zaddscl  28596  zmulscld  28599  zseo  28624  z12addscl  28679  tglngval  28829  islnopp  29029  ishpg  29050  elplngid  29073  lnincplng  29075  plngcp  29077  plngrot  29081  nhpmirhp  29089  lnperpexs  29123  ragraghl  29158  prlnghpg  29205  prlngmo  29213  finsumvtxdg2size  29909  wspthsn  30206  wwlksnon  30209  wspthsnon  30210  iswspthsnon  30214  2clwwlk  30707  numclwlk1lem2  30730  numclwwlkovh0  30732  hmoval  31171  htth  31279  normval  31485  hlimi  31549  hsn0elch  31609  ocsh  31644  shscli  31678  shs00i  31811  chj00i  31848  riesz4i  32424  stm1addi  32606  stm1add3i  32608  superpos  32715  elrgspnlem2  33572  drnglring  33791  idlsrgmulrval  33808  splyval  33958  brfinext  34051  finextfldext  34063  irngval  34084  minplyval  34104  submateq  34208  metidv  34291  rmulccn  34327  pl1cn  34354  sibfof  34739  cxpcncf1  34991  subfacval2  35687  txsconnlem  35740  cvxpconn  35742  cvxsconn  35743  iscvm  35759  prv  35928  mpomulnzcnf  36839  knoppcnlem10  37119  bj-bary1  37984  ismblfin  38340  itg2addnclem3  38352  itg2addnc  38353  ftc1anclem3  38374  ftc1anc  38380  bfp  38503  rngo2  38586  rngohomco  38653  rngoisoval  38656  rngoisocnv  38660  crngohomfo  38685  keridl  38711  ispridlc  38749  snatpsubN  40552  cdlemn11pre  42012  dihord2pre  42027  baerlem3lem1  42509  prjcrvfval  43391  mendval  43934  mendplusg  43937  omcl3g  44089  mulvval  45204  fprodcnlem  46343  climf  46366  climf2  46408  cxpcncf2  46641  smflimlem3  47515  fmtnofac2lem  48348  prmdvdsfmtnof1lem2  48365  opoeALTV  48476  opeoALTV  48477  rngchomALTV  49061  funcringcsetcALTV2lem5  49087  ringchomALTV  49095  funcringcsetclem5ALTV  49110  srhmsubcALTVlem2  49117  srhmsubcALTV  49118  fldhmsubcALTV  49126  dmatALTval  49208  lincsumcl  49239  fdivval  49347  catprslem  49816  catprsc  49819  catprsc2  49820  oppcendc  49824  thincmoALT  50235  functhinclem2  50251  fullthinc2  50257  setc1onsubc  50408  lmdfval  50455  cmdfval  50456