Theorem oveq12 7358

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  oveq12i  7361  oveq12d  7367  oveqan12d  7368  ovmpot  7510  mptmpoopabovd  8017  suppofssd  8136  sprmpod  8157  oev2  8441  oa00  8477  omopthi  8579  ecopoveq  8745  ecopovtrn  8747  isfsupp  9255  cantnffval  9559  ttrcltr  9612  fpwwe2lem4  10528  fpwwe2  10537  pwfseqlem4  10556  halfnq  10870  distrlem5pr  10921  addcmpblnr  10963  ltsrpr  10971  mulgt0sr  10999  add20  11632  msqge0  11641  recextlem2  11751  cru  12120  zaddcl  12515  qaddcl  12866  qmulcl  12868  xaddval  13125  xmulval  13127  xnn0xadd0  13149  xadddilem  13196  fzopth  13464  fzoopth  13665  modval  13775  1exp  13998  m1expeven  14016  nn0opthi  14177  faclbnd  14197  faclbnd3  14199  bcn0  14217  ccatopth  14622  ccatopth2  14623  repswccat  14692  reval  15013  absval  15145  clim  15401  rlim  15402  fsumparts  15713  cpnnen  16138  dvds2add  16201  dvds2sub  16202  opoe  16274  omoe  16275  opeo  16276  omeo  16277  gcddvds  16414  gcdcl  16417  gcdeq0  16428  gcdneg  16433  gcdaddmlem  16435  bezoutlem3  16452  bezout  16454  gcddiv  16462  nn0rppwr  16472  eucalgval2  16492  lcmabs  16516  rpmul  16570  divgcdcoprmex  16577  isprm5  16618  prmexpb  16630  rpexp  16633  nn0gcdsq  16663  pcqmul  16765  prmreclem3  16830  mul4sq  16866  vdwapval  16885  f1ocpbl  17429  homfval  17598  comfval  17606  issect  17660  isfull  17819  isfth  17823  natfval  17856  catchom  18010  catcco  18012  funcsetcestrclem5  18065  plusfval  18521  0subm  18691  cycsubm  19081  cyccom  19082  isgim  19141  subgga  19179  cayleylem1  19291  lsmsubm  19532  subgdisjb  19572  pj1fval  19573  odadd1  19727  qusabl  19744  imasabl  19755  dprdsubg  19905  rnghmval  20325  isrngim  20330  dfrhm2  20359  isrhm  20363  isrim0OLD  20366  isrim0  20368  rhmval  20385  funcrngcsetcALT  20526  srhmsubclem3  20564  srhmsubc  20565  fldhmsubc  20670  scafval  20784  rmodislmodlem  20832  rmodislmod  20833  lss1d  20866  islmhm  20931  islmim  20966  pzriprnglem5  21392  pzriprnglem8  21395  znfld  21467  cygznlem3  21476  cnmsgnsubg  21484  psgnghm  21487  ipeq0  21545  ipfval  21556  dsmmval  21641  dsmmacl  21648  mplval  21896  mplcoe5lem  21944  opsrval  21951  evlval  22000  mpfind  22012  selvffval  22018  mhpfval  22023  mhpmulcl  22034  psdffval  22042  mat1dimcrng  22362  dmatval  22377  dmatmulcl  22385  scmatval  22389  scmataddcl  22401  scmatsubcl  22402  scmatmulcl  22403  mavmul0g  22438  marrepfval  22445  marrepeval  22448  marepvfval  22450  marepveval  22453  submafval  22464  submaeval  22467  mdetfval  22471  madugsum  22528  minmar1fval  22531  minmar1eval  22534  symgmatr01  22539  gsummatr01lem3  22542  gsummatr01lem4  22543  gsummatr01  22544  cpmatacl  22601  mat2pmatfval  22608  mat2pmatvalel  22610  mat2pmatmul  22616  cpm2mfval  22634  cpm2mvalel  22636  m2cpminvid  22638  m2cpminvid2  22640  decpmate  22651  pmatcollpw1  22661  monmatcollpw  22664  pmatcollpwlem  22665  pmatcollpw  22666  pmatcollpwscmatlem2  22675  pm2mpval  22680  pm2mpf1  22684  mp2pm2mplem3  22693  mp2pm2mplem4  22694  chpmatfval  22715  tx2ndc  23536  cnmpt2t  23558  cnmpt22f  23560  hmeofval  23643  qustgplem  24006  stdbdmetval  24400  nmofval  24600  nghmfval  24608  isnmhm  24632  xrsxmet  24696  divcn  24757  divccn  24762  iihalf1cn  24824  iihalf2cn  24827  icchmeo  24836  cnrehmeo  24849  isphtpy  24878  isphtpc  24891  reparphti  24894  pcorevlem  24924  cphnm  25091  tcphnmval  25127  ipcau2  25132  tcphcphlem1  25133  tcphcphlem2  25134  tcphcph  25135  bcthlem1  25222  bcth  25227  mulcncf  25344  dyadmax  25497  volcn  25505  vitalilem1  25507  vitalilem2  25508  vitalilem3  25509  vitali  25512  i1fmullem  25593  itg1addlem4  25598  dvlip  25896  ftc1a  25942  mdegfval  25965  r1pval  26061  coeaddlem  26152  plycn  26164  quotval  26198  elqaalem2  26226  taylfval  26264  psercn2  26330  cxpcn  26652  cxpcn3  26656  resqrtcn  26657  sqrtcn  26658  abscxpbnd  26661  angval  26709  chordthmlem  26740  dcubic  26754  efrlim  26877  lgsdchr  27264  mul2sq  27328  ostthlem2  27537  zaddscl  28287  zmulscld  28290  zseo  28314  zs12addscl  28354  tglngval  28496  islnopp  28684  ishpg  28704  finsumvtxdg2size  29496  wspthsn  29793  wwlksnon  29796  wspthsnon  29797  iswspthsnon  29801  2clwwlk  30291  numclwlk1lem2  30314  numclwwlkovh0  30316  hmoval  30754  htth  30862  normval  31068  hlimi  31132  hsn0elch  31192  ocsh  31227  shscli  31261  shs00i  31394  chj00i  31431  riesz4i  32007  stm1addi  32189  stm1add3i  32191  superpos  32298  elrgspnlem2  33184  prmidlc  33386  idlsrgmulrval  33447  splyval  33552  brfinext  33625  finextfldext  33637  irngval  33658  minplyval  33678  submateq  33782  metidv  33865  rmulccn  33901  pl1cn  33928  sibfof  34314  cxpcncf1  34569  subfacval2  35170  txsconnlem  35223  cvxpconn  35225  cvxsconn  35226  iscvm  35242  prv  35411  mpomulnzcnf  36283  knoppcnlem10  36486  bj-bary1  37296  ismblfin  37651  itg2addnclem3  37663  itg2addnc  37664  ftc1anclem3  37685  ftc1anc  37691  bfp  37814  rngo2  37897  rngohomco  37964  rngoisoval  37967  rngoisocnv  37971  crngohomfo  37996  keridl  38022  ispridlc  38060  snatpsubN  39739  cdlemn11pre  41199  dihord2pre  41214  baerlem3lem1  41696  prjcrvfval  42614  mendval  43162  mendplusg  43165  omcl3g  43317  mulvval  44451  fprodcnlem  45590  climf  45613  climf2  45657  cxpcncf2  45890  smflimlem3  46764  fmtnofac2lem  47562  prmdvdsfmtnof1lem2  47579  opoeALTV  47677  opeoALTV  47678  rngchomALTV  48262  funcringcsetcALTV2lem5  48288  ringchomALTV  48296  funcringcsetclem5ALTV  48311  srhmsubcALTVlem2  48318  srhmsubcALTV  48319  fldhmsubcALTV  48327  dmatALTval  48395  lincsumcl  48426  fdivval  48534  catprslem  49005  catprsc  49008  catprsc2  49009  oppcendc  49013  thincmoALT  49424  functhinclem2  49440  fullthinc2  49446  setc1onsubc  49597  lmdfval  49644  cmdfval  49645