Theorem oveq12 7415

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

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

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409

This theorem is referenced by:  oveq12i  7418  oveq12d  7424  oveqan12d  7425  mptmpoopabovd  8065  mptmpoopabovdOLD  8067  suppofssd  8185  sprmpod  8206  oev2  8520  oa00  8556  omopthi  8657  ecopoveq  8809  ecopovtrn  8811  isfsupp  9362  cantnffval  9655  ttrcltr  9708  fpwwe2  10635  halfnq  10968  distrlem5pr  11019  addcmpblnr  11061  ltsrpr  11069  mulgt0sr  11097  add20  11723  msqge0  11732  recextlem2  11842  cru  12201  zaddcl  12599  qaddcl  12946  qmulcl  12948  xaddval  13199  xmulval  13201  xnn0xadd0  13223  xadddilem  13270  fzopth  13535  modval  13833  1exp  14054  m1expeven  14072  nn0opthi  14227  faclbnd  14247  faclbnd3  14249  bcn0  14267  ccatopth  14663  ccatopth2  14664  repswccat  14733  reval  15050  absval  15182  clim  15435  rlim  15436  fsumparts  15749  cpnnen  16169  dvds2add  16230  dvds2sub  16231  opoe  16303  omoe  16304  opeo  16305  omeo  16306  gcddvds  16441  gcdcl  16444  gcdeq0  16455  gcdneg  16460  gcdaddmlem  16462  gcdabsOLD  16470  bezoutlem3  16480  bezout  16482  gcddiv  16490  eucalgval2  16515  lcmabs  16539  rpmul  16593  divgcdcoprmex  16600  isprm5  16641  prmexpb  16654  rpexp  16656  nn0gcdsq  16685  pcqmul  16783  prmreclem3  16848  mul4sq  16884  vdwapval  16903  f1ocpbl  17468  homfval  17633  comfval  17641  issect  17697  isfull  17858  isfth  17862  natfval  17894  catchom  18050  catcco  18052  funcsetcestrclem5  18108  plusfval  18565  0subm  18695  cycsubm  19074  cyccom  19075  isgim  19131  subgga  19159  cayleylem1  19275  lsmsubm  19516  subgdisjb  19556  pj1fval  19557  odadd1  19711  qusabl  19728  imasabl  19739  dprdsubg  19889  dfrhm2  20246  isrhm  20250  isrim0OLD  20252  isrim0  20254  scafval  20484  rmodislmodlem  20532  rmodislmod  20533  rmodislmodOLD  20534  lss1d  20567  islmhm  20631  islmim  20666  znfld  21108  cygznlem3  21117  cnmsgnsubg  21122  psgnghm  21125  ipeq0  21183  ipfval  21194  dsmmval  21281  dsmmacl  21288  mplval  21540  mplcoe5lem  21586  opsrval  21593  evlval  21650  mpfind  21662  selvffval  21671  mhpfval  21674  mhpmulcl  21684  mat1dimcrng  21971  dmatval  21986  dmatmulcl  21994  scmatval  21998  scmataddcl  22010  scmatsubcl  22011  scmatmulcl  22012  mavmul0g  22047  marrepfval  22054  marrepeval  22057  marepvfval  22059  marepveval  22062  submafval  22073  submaeval  22076  mdetfval  22080  madugsum  22137  minmar1fval  22140  minmar1eval  22143  symgmatr01  22148  gsummatr01lem3  22151  gsummatr01lem4  22152  gsummatr01  22153  cpmatacl  22210  mat2pmatfval  22217  mat2pmatvalel  22219  mat2pmatmul  22225  cpm2mfval  22243  cpm2mvalel  22245  m2cpminvid  22247  m2cpminvid2  22249  decpmate  22260  pmatcollpw1  22270  monmatcollpw  22273  pmatcollpwlem  22274  pmatcollpw  22275  pmatcollpwscmatlem2  22284  pm2mpval  22289  pm2mpf1  22293  mp2pm2mplem3  22302  mp2pm2mplem4  22303  chpmatfval  22324  tx2ndc  23147  cnmpt2t  23169  cnmpt22f  23171  hmeofval  23254  qustgplem  23617  stdbdmetval  24015  nmofval  24223  nghmfval  24231  isnmhm  24255  xrsxmet  24317  isphtpy  24489  isphtpc  24502  pcorevlem  24534  cphnm  24702  tcphnmval  24738  ipcau2  24743  tcphcphlem1  24744  tcphcphlem2  24745  tcphcph  24746  bcthlem1  24833  bcth  24838  dyadmax  25107  volcn  25115  vitalilem1  25117  vitalilem2  25118  vitalilem3  25119  vitali  25122  i1fmullem  25203  itg1addlem4  25208  itg1addlem4OLD  25209  dvlip  25502  ftc1a  25546  mdegfval  25572  r1pval  25666  coeaddlem  25755  quotval  25797  elqaalem2  25825  taylfval  25863  cxpcn3  26246  resqrtcn  26247  sqrtcn  26248  abscxpbnd  26251  angval  26296  chordthmlem  26327  dcubic  26341  lgsdchr  26848  mul2sq  26912  ostthlem2  27121  tglngval  27792  islnopp  27980  ishpg  28000  finsumvtxdg2size  28797  wspthsn  29092  wwlksnon  29095  wspthsnon  29096  iswspthsnon  29100  2clwwlk  29590  numclwlk1lem2  29613  numclwwlkovh0  29615  hmoval  30051  htth  30159  normval  30365  hlimi  30429  hsn0elch  30489  ocsh  30524  shscli  30558  shs00i  30691  chj00i  30728  riesz4i  31304  stm1addi  31486  stm1add3i  31488  superpos  31595  prmidlc  32556  idlsrgmulrval  32612  brfinext  32721  irngval  32738  minplyval  32755  submateq  32778  metidv  32861  rmulccn  32897  pl1cn  32924  sibfof  33328  cxpcncf1  33596  subfacval2  34167  txsconnlem  34220  iscvm  34239  prv  34408  ovmul  35149  gg-divcn  35152  gg-divccn  35154  gg-iihalf1cn  35156  gg-iihalf2cn  35157  gg-icchmeo  35159  gg-cnrehmeo  35160  gg-reparphti  35161  gg-mulcncf  35162  gg-plycn  35166  gg-psercn2  35167  gg-rmulccn  35168  gg-cxpcn  35173  bj-bary1  36182  ismblfin  36518  itg2addnclem3  36530  itg2addnc  36531  ftc1anclem3  36552  ftc1anc  36558  bfp  36681  rngo2  36764  rngohomco  36831  rngoisoval  36834  rngoisocnv  36838  crngohomfo  36863  keridl  36889  ispridlc  36927  snatpsubN  38610  cdlemn11pre  40070  dihord2pre  40085  baerlem3lem1  40567  nn0rppwr  41220  sn-inelr  41335  prjcrvfval  41370  mendval  41911  mendplusg  41914  omcl3g  42070  mulvval  43213  climf  44325  climf2  44369  cxpcncf2  44602  smflimlem3  45476  fzoopth  46022  fmtnofac2lem  46223  prmdvdsfmtnof1lem2  46240  opoeALTV  46338  opeoALTV  46339  rnghmval  46675  isrngisom  46680  rhmval  46707  rngchomALTV  46837  funcrngcsetcALT  46851  funcringcsetcALTV2lem5  46892  ringchomALTV  46900  funcringcsetclem5ALTV  46915  srhmsubclem3  46927  srhmsubc  46928  fldhmsubc  46936  srhmsubcALTVlem2  46945  srhmsubcALTV  46946  fldhmsubcALTV  46954  dmatALTval  47035  lincsumcl  47066  fdivval  47179  catprslem  47584  catprsc  47587  catprsc2  47588  thincmoALT  47604  functhinclem2  47616  fullthinc2  47621