Theorem oveq12 6067

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  oveq12i  6070  oveq12d  6076  oveqan12d  6077  ecopoveq  6877  ecopovtrn  6879  ecopovtrng  6882  th3qlem1  6884  th3qlem2  6885  isfsupp  7255  mulcmpblnq  7699  addpipqqs  7701  ordpipqqs  7705  enq0breq  7767  mulcmpblnq0  7775  nqpnq0nq  7784  nqnq0a  7785  nqnq0m  7786  nq0m0r  7787  nq0a0  7788  distrlem5prl  7917  distrlem5pru  7918  addcmpblnr  8070  ltsrprg  8078  mulgt0sr  8109  add20  8765  cru  8893  qaddcl  9985  qmulcl  9987  xaddval  10197  xnn0xadd0  10219  fzopth  10416  modqval  10710  seqvalcd  10847  seqovcd  10853  1exp  10954  m1expeven  10972  nn0opthd  11109  faclbnd  11128  faclbnd3  11130  bcn0  11142  ccatopth  11433  ccatopth2  11434  reval  11559  absval  11711  clim  11991  fsumparts  12181  dvds2add  12536  dvds2sub  12537  opoe  12606  omoe  12607  opeo  12608  omeo  12609  gcddvds  12684  gcdcl  12687  gcdeq0  12698  gcdneg  12703  gcdaddm  12705  gcdabs  12709  gcddiv  12740  eucalgval2  12775  lcmabs  12798  rpmul  12820  divgcdcoprmex  12824  prmexpb  12873  rpexp  12875  nn0gcdsq  12922  pcqmul  13026  mul4sq  13117  f1ocpbl  13575  plusfvalg  13626  0subm  13739  imasabl  14089  ringadd2  14270  dfrhm2  14399  isrhm  14403  isrim0  14406  rhmval  14418  aprval  14529  scafvalg  14581  rmodislmodlem  14624  rmodislmod  14625  lss1d  14657  znidom  14931  mplvalcoe  14971  cnmpt2t  15284  cnmpt22f  15286  hmeofvalg  15294  bdmetval  15491  plycn  15753  mul2sq  16115