Theorem oveq12 7441

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435

This theorem is referenced by:  oveq12i  7444  oveq12d  7450  oveqan12d  7451  ovmpot  7595  mptmpoopabovd  8108  mptmpoopabovdOLD  8110  suppofssd  8229  sprmpod  8250  oev2  8562  oa00  8598  omopthi  8700  ecopoveq  8859  ecopovtrn  8861  isfsupp  9406  cantnffval  9704  ttrcltr  9757  fpwwe2lem4  10675  fpwwe2  10684  pwfseqlem4  10703  halfnq  11017  distrlem5pr  11068  addcmpblnr  11110  ltsrpr  11118  mulgt0sr  11146  add20  11776  msqge0  11785  recextlem2  11895  cru  12259  zaddcl  12659  qaddcl  13008  qmulcl  13010  xaddval  13266  xmulval  13268  xnn0xadd0  13290  xadddilem  13337  fzopth  13602  fzoopth  13802  modval  13912  1exp  14133  m1expeven  14151  nn0opthi  14310  faclbnd  14330  faclbnd3  14332  bcn0  14350  ccatopth  14755  ccatopth2  14756  repswccat  14825  reval  15146  absval  15278  clim  15531  rlim  15532  fsumparts  15843  cpnnen  16266  dvds2add  16328  dvds2sub  16329  opoe  16401  omoe  16402  opeo  16403  omeo  16404  gcddvds  16541  gcdcl  16544  gcdeq0  16555  gcdneg  16560  gcdaddmlem  16562  bezoutlem3  16579  bezout  16581  gcddiv  16589  nn0rppwr  16599  eucalgval2  16619  lcmabs  16643  rpmul  16697  divgcdcoprmex  16704  isprm5  16745  prmexpb  16757  rpexp  16760  nn0gcdsq  16790  pcqmul  16892  prmreclem3  16957  mul4sq  16993  vdwapval  17012  f1ocpbl  17571  homfval  17736  comfval  17744  issect  17798  isfull  17958  isfth  17962  natfval  17995  catchom  18149  catcco  18151  funcsetcestrclem5  18205  plusfval  18661  0subm  18831  cycsubm  19221  cyccom  19222  isgim  19281  subgga  19319  cayleylem1  19431  lsmsubm  19672  subgdisjb  19712  pj1fval  19713  odadd1  19867  qusabl  19884  imasabl  19895  dprdsubg  20045  rnghmval  20441  isrngim  20446  dfrhm2  20475  isrhm  20479  isrim0OLD  20482  isrim0  20484  rhmval  20501  funcrngcsetcALT  20642  srhmsubclem3  20680  srhmsubc  20681  fldhmsubc  20787  scafval  20880  rmodislmodlem  20928  rmodislmod  20929  lss1d  20962  islmhm  21027  islmim  21062  pzriprnglem5  21497  pzriprnglem8  21500  znfld  21580  cygznlem3  21589  cnmsgnsubg  21596  psgnghm  21599  ipeq0  21657  ipfval  21668  dsmmval  21755  dsmmacl  21762  mplval  22010  mplcoe5lem  22058  opsrval  22065  evlval  22120  mpfind  22132  selvffval  22138  mhpfval  22143  mhpmulcl  22154  psdffval  22162  mat1dimcrng  22484  dmatval  22499  dmatmulcl  22507  scmatval  22511  scmataddcl  22523  scmatsubcl  22524  scmatmulcl  22525  mavmul0g  22560  marrepfval  22567  marrepeval  22570  marepvfval  22572  marepveval  22575  submafval  22586  submaeval  22589  mdetfval  22593  madugsum  22650  minmar1fval  22653  minmar1eval  22656  symgmatr01  22661  gsummatr01lem3  22664  gsummatr01lem4  22665  gsummatr01  22666  cpmatacl  22723  mat2pmatfval  22730  mat2pmatvalel  22732  mat2pmatmul  22738  cpm2mfval  22756  cpm2mvalel  22758  m2cpminvid  22760  m2cpminvid2  22762  decpmate  22773  pmatcollpw1  22783  monmatcollpw  22786  pmatcollpwlem  22787  pmatcollpw  22788  pmatcollpwscmatlem2  22797  pm2mpval  22802  pm2mpf1  22806  mp2pm2mplem3  22815  mp2pm2mplem4  22816  chpmatfval  22837  tx2ndc  23660  cnmpt2t  23682  cnmpt22f  23684  hmeofval  23767  qustgplem  24130  stdbdmetval  24528  nmofval  24736  nghmfval  24744  isnmhm  24768  xrsxmet  24832  divcn  24893  divccn  24898  iihalf1cn  24960  iihalf2cn  24963  icchmeo  24972  cnrehmeo  24985  isphtpy  25014  isphtpc  25027  reparphti  25030  pcorevlem  25060  cphnm  25228  tcphnmval  25264  ipcau2  25269  tcphcphlem1  25270  tcphcphlem2  25271  tcphcph  25272  bcthlem1  25359  bcth  25364  mulcncf  25481  dyadmax  25634  volcn  25642  vitalilem1  25644  vitalilem2  25645  vitalilem3  25646  vitali  25649  i1fmullem  25730  itg1addlem4  25735  dvlip  26033  ftc1a  26079  mdegfval  26102  r1pval  26198  coeaddlem  26289  plycn  26301  quotval  26335  elqaalem2  26363  taylfval  26401  psercn2  26467  cxpcn  26788  cxpcn3  26792  resqrtcn  26793  sqrtcn  26794  abscxpbnd  26797  angval  26845  chordthmlem  26876  dcubic  26890  efrlim  27013  lgsdchr  27400  mul2sq  27464  ostthlem2  27673  zaddscl  28381  zmulscld  28384  zseo  28407  tglngval  28560  islnopp  28748  ishpg  28768  finsumvtxdg2size  29569  wspthsn  29869  wwlksnon  29872  wspthsnon  29873  iswspthsnon  29877  2clwwlk  30367  numclwlk1lem2  30390  numclwwlkovh0  30392  hmoval  30830  htth  30938  normval  31144  hlimi  31208  hsn0elch  31268  ocsh  31303  shscli  31337  shs00i  31470  chj00i  31507  riesz4i  32083  stm1addi  32265  stm1add3i  32267  superpos  32374  elrgspnlem2  33248  prmidlc  33477  idlsrgmulrval  33538  brfinext  33705  irngval  33736  minplyval  33749  submateq  33809  metidv  33892  rmulccn  33928  pl1cn  33955  sibfof  34343  cxpcncf1  34611  subfacval2  35193  txsconnlem  35246  cvxpconn  35248  cvxsconn  35249  iscvm  35265  prv  35434  mpomulnzcnf  36301  knoppcnlem10  36504  bj-bary1  37314  ismblfin  37669  itg2addnclem3  37681  itg2addnc  37682  ftc1anclem3  37703  ftc1anc  37709  bfp  37832  rngo2  37915  rngohomco  37982  rngoisoval  37985  rngoisocnv  37989  crngohomfo  38014  keridl  38040  ispridlc  38078  snatpsubN  39753  cdlemn11pre  41213  dihord2pre  41228  baerlem3lem1  41710  sn-inelr  42502  prjcrvfval  42646  mendval  43196  mendplusg  43199  omcl3g  43352  mulvval  44492  fprodcnlem  45619  climf  45642  climf2  45686  cxpcncf2  45919  smflimlem3  46793  fmtnofac2lem  47560  prmdvdsfmtnof1lem2  47577  opoeALTV  47675  opeoALTV  47676  rngchomALTV  48189  funcringcsetcALTV2lem5  48215  ringchomALTV  48223  funcringcsetclem5ALTV  48238  srhmsubcALTVlem2  48245  srhmsubcALTV  48246  fldhmsubcALTV  48254  dmatALTval  48322  lincsumcl  48353  fdivval  48465  catprslem  48914  catprsc  48917  catprsc2  48918  oppcendc  48921  thincmoALT  49103  functhinclem2  49119  fullthinc2  49125