Theorem oveq12 7457

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  oveq12i  7460  oveq12d  7466  oveqan12d  7467  ovmpot  7611  mptmpoopabovd  8123  mptmpoopabovdOLD  8125  suppofssd  8244  sprmpod  8265  oev2  8579  oa00  8615  omopthi  8717  ecopoveq  8876  ecopovtrn  8878  isfsupp  9435  cantnffval  9732  ttrcltr  9785  fpwwe2lem4  10703  fpwwe2  10712  pwfseqlem4  10731  halfnq  11045  distrlem5pr  11096  addcmpblnr  11138  ltsrpr  11146  mulgt0sr  11174  add20  11802  msqge0  11811  recextlem2  11921  cru  12285  zaddcl  12683  qaddcl  13030  qmulcl  13032  xaddval  13285  xmulval  13287  xnn0xadd0  13309  xadddilem  13356  fzopth  13621  fzoopth  13812  modval  13922  1exp  14142  m1expeven  14160  nn0opthi  14319  faclbnd  14339  faclbnd3  14341  bcn0  14359  ccatopth  14764  ccatopth2  14765  repswccat  14834  reval  15155  absval  15287  clim  15540  rlim  15541  fsumparts  15854  cpnnen  16277  dvds2add  16338  dvds2sub  16339  opoe  16411  omoe  16412  opeo  16413  omeo  16414  gcddvds  16549  gcdcl  16552  gcdeq0  16563  gcdneg  16568  gcdaddmlem  16570  gcdabsOLD  16578  bezoutlem3  16588  bezout  16590  gcddiv  16598  nn0rppwr  16608  eucalgval2  16628  lcmabs  16652  rpmul  16706  divgcdcoprmex  16713  isprm5  16754  prmexpb  16766  rpexp  16769  nn0gcdsq  16799  pcqmul  16900  prmreclem3  16965  mul4sq  17001  vdwapval  17020  f1ocpbl  17585  homfval  17750  comfval  17758  issect  17814  isfull  17977  isfth  17981  natfval  18014  catchom  18170  catcco  18172  funcsetcestrclem5  18228  plusfval  18685  0subm  18852  cycsubm  19242  cyccom  19243  isgim  19302  subgga  19340  cayleylem1  19454  lsmsubm  19695  subgdisjb  19735  pj1fval  19736  odadd1  19890  qusabl  19907  imasabl  19918  dprdsubg  20068  rnghmval  20466  isrngim  20471  dfrhm2  20500  isrhm  20504  isrim0OLD  20507  isrim0  20509  rhmval  20526  funcrngcsetcALT  20663  srhmsubclem3  20701  srhmsubc  20702  fldhmsubc  20808  scafval  20901  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  lss1d  20984  islmhm  21049  islmim  21084  pzriprnglem5  21519  pzriprnglem8  21522  znfld  21602  cygznlem3  21611  cnmsgnsubg  21618  psgnghm  21621  ipeq0  21679  ipfval  21690  dsmmval  21777  dsmmacl  21784  mplval  22032  mplcoe5lem  22080  opsrval  22087  evlval  22142  mpfind  22154  selvffval  22160  mhpfval  22165  mhpmulcl  22176  psdffval  22184  mat1dimcrng  22504  dmatval  22519  dmatmulcl  22527  scmatval  22531  scmataddcl  22543  scmatsubcl  22544  scmatmulcl  22545  mavmul0g  22580  marrepfval  22587  marrepeval  22590  marepvfval  22592  marepveval  22595  submafval  22606  submaeval  22609  mdetfval  22613  madugsum  22670  minmar1fval  22673  minmar1eval  22676  symgmatr01  22681  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  cpmatacl  22743  mat2pmatfval  22750  mat2pmatvalel  22752  mat2pmatmul  22758  cpm2mfval  22776  cpm2mvalel  22778  m2cpminvid  22780  m2cpminvid2  22782  decpmate  22793  pmatcollpw1  22803  monmatcollpw  22806  pmatcollpwlem  22807  pmatcollpw  22808  pmatcollpwscmatlem2  22817  pm2mpval  22822  pm2mpf1  22826  mp2pm2mplem3  22835  mp2pm2mplem4  22836  chpmatfval  22857  tx2ndc  23680  cnmpt2t  23702  cnmpt22f  23704  hmeofval  23787  qustgplem  24150  stdbdmetval  24548  nmofval  24756  nghmfval  24764  isnmhm  24788  xrsxmet  24850  divcn  24911  divccn  24916  iihalf1cn  24978  iihalf2cn  24981  icchmeo  24990  cnrehmeo  25003  isphtpy  25032  isphtpc  25045  reparphti  25048  pcorevlem  25078  cphnm  25246  tcphnmval  25282  ipcau2  25287  tcphcphlem1  25288  tcphcphlem2  25289  tcphcph  25290  bcthlem1  25377  bcth  25382  mulcncf  25499  dyadmax  25652  volcn  25660  vitalilem1  25662  vitalilem2  25663  vitalilem3  25664  vitali  25667  i1fmullem  25748  itg1addlem4  25753  itg1addlem4OLD  25754  dvlip  26052  ftc1a  26098  mdegfval  26121  r1pval  26217  coeaddlem  26308  plycn  26320  quotval  26352  elqaalem2  26380  taylfval  26418  psercn2  26484  cxpcn  26805  cxpcn3  26809  resqrtcn  26810  sqrtcn  26811  abscxpbnd  26814  angval  26862  chordthmlem  26893  dcubic  26907  efrlim  27030  lgsdchr  27417  mul2sq  27481  ostthlem2  27690  zaddscl  28398  zmulscld  28401  zseo  28424  tglngval  28577  islnopp  28765  ishpg  28785  finsumvtxdg2size  29586  wspthsn  29881  wwlksnon  29884  wspthsnon  29885  iswspthsnon  29889  2clwwlk  30379  numclwlk1lem2  30402  numclwwlkovh0  30404  hmoval  30842  htth  30950  normval  31156  hlimi  31220  hsn0elch  31280  ocsh  31315  shscli  31349  shs00i  31482  chj00i  31519  riesz4i  32095  stm1addi  32277  stm1add3i  32279  superpos  32386  prmidlc  33441  idlsrgmulrval  33502  brfinext  33666  irngval  33685  minplyval  33698  fldext2chn  33719  submateq  33755  metidv  33838  rmulccn  33874  pl1cn  33901  sibfof  34305  cxpcncf1  34572  subfacval2  35155  txsconnlem  35208  cvxpconn  35210  cvxsconn  35211  iscvm  35227  prv  35396  mpomulnzcnf  36265  knoppcnlem10  36468  bj-bary1  37278  ismblfin  37621  itg2addnclem3  37633  itg2addnc  37634  ftc1anclem3  37655  ftc1anc  37661  bfp  37784  rngo2  37867  rngohomco  37934  rngoisoval  37937  rngoisocnv  37941  crngohomfo  37966  keridl  37992  ispridlc  38030  snatpsubN  39707  cdlemn11pre  41167  dihord2pre  41182  baerlem3lem1  41664  sn-inelr  42443  prjcrvfval  42586  mendval  43140  mendplusg  43143  omcl3g  43296  mulvval  44437  fprodcnlem  45520  climf  45543  climf2  45587  cxpcncf2  45820  smflimlem3  46694  fmtnofac2lem  47442  prmdvdsfmtnof1lem2  47459  opoeALTV  47557  opeoALTV  47558  rngchomALTV  47991  funcringcsetcALTV2lem5  48017  ringchomALTV  48025  funcringcsetclem5ALTV  48040  srhmsubcALTVlem2  48047  srhmsubcALTV  48048  fldhmsubcALTV  48056  dmatALTval  48129  lincsumcl  48160  fdivval  48273  catprslem  48677  catprsc  48680  catprsc2  48681  thincmoALT  48697  functhinclem2  48709  fullthinc2  48714