Theorem oveq12 6059

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  (class class class)co 6050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053

This theorem is referenced by:  oveq12i  6062  oveq12d  6068  oveqan12d  6069  ecopoveq  6864  ecopovtrn  6866  ecopovtrng  6869  th3qlem1  6871  th3qlem2  6872  isfsupp  7242  mulcmpblnq  7683  addpipqqs  7685  ordpipqqs  7689  enq0breq  7751  mulcmpblnq0  7759  nqpnq0nq  7768  nqnq0a  7769  nqnq0m  7770  nq0m0r  7771  nq0a0  7772  distrlem5prl  7901  distrlem5pru  7902  addcmpblnr  8054  ltsrprg  8062  mulgt0sr  8093  add20  8748  cru  8876  qaddcl  9967  qmulcl  9969  xaddval  10178  xnn0xadd0  10200  fzopth  10395  modqval  10686  seqvalcd  10823  seqovcd  10829  1exp  10930  m1expeven  10948  nn0opthd  11084  faclbnd  11103  faclbnd3  11105  bcn0  11117  ccatopth  11408  ccatopth2  11409  reval  11534  absval  11686  clim  11966  fsumparts  12156  dvds2add  12511  dvds2sub  12512  opoe  12581  omoe  12582  opeo  12583  omeo  12584  gcddvds  12659  gcdcl  12662  gcdeq0  12673  gcdneg  12678  gcdaddm  12680  gcdabs  12684  gcddiv  12715  eucalgval2  12750  lcmabs  12773  rpmul  12795  divgcdcoprmex  12799  prmexpb  12848  rpexp  12850  nn0gcdsq  12897  pcqmul  13001  mul4sq  13092  f1ocpbl  13524  plusfvalg  13576  0subm  13697  imasabl  14053  ringadd2  14171  dfrhm2  14299  isrhm  14303  isrim0  14306  rhmval  14318  aprval  14428  scafvalg  14455  rmodislmodlem  14498  rmodislmod  14499  lss1d  14531  znidom  14805  mplvalcoe  14845  cnmpt2t  15158  cnmpt22f  15160  hmeofvalg  15168  bdmetval  15365  plycn  15627  mul2sq  15989