Theorem oveq12 6097

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402  (class class class)co 6088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  oveq12i  6100  oveq12d  6106  oveqan12d  6107  ecopoveq  6908  ecopovtrn  6910  ecopovtrng  6913  th3qlem1  6915  th3qlem2  6916  isfsupp  7294  mulcmpblnq  7741  addpipqqs  7743  ordpipqqs  7747  enq0breq  7809  mulcmpblnq0  7817  nqpnq0nq  7826  nqnq0a  7827  nqnq0m  7828  nq0m0r  7829  nq0a0  7830  distrlem5prl  7959  distrlem5pru  7960  addcmpblnr  8112  ltsrprg  8120  mulgt0sr  8151  add20  8809  cru  8938  qaddcl  10051  qmulcl  10053  xaddval  10264  xnn0xadd0  10286  fzopth  10484  modqval  10782  seqvalcd  10919  seqovcd  10925  1exp  11026  m1expeven  11044  nn0opthd  11182  faclbnd  11201  faclbnd3  11203  bcn0  11215  ccatopth  11510  ccatopth2  11511  reval  11636  absval  11789  clim  12072  fsumparts  12262  dvds2add  12617  dvds2sub  12618  opoe  12687  omoe  12688  opeo  12689  omeo  12690  gcddvds  12765  gcdcl  12768  gcdeq0  12779  gcdneg  12784  gcdaddm  12786  gcdabs  12790  gcddiv  12821  eucalgval2  12856  lcmabs  12879  rpmul  12901  divgcdcoprmex  12905  prmexpb  12955  rpexp  12957  nn0gcdsq  13005  pcqmul  13111  mul4sq  13202  f1ocpbl  13691  plusfvalg  13742  0subm  13850  imasabl  14230  ringadd2  14439  dfrhm2  14570  isrhm  14574  isrim0  14577  rhmval  14589  aprval  14700  scafvalg  14753  rmodislmodlem  14796  rmodislmod  14797  lss1d  14829  znidom  15101  mplvalcoe  15206  cnmpt2t  15519  cnmpt22f  15521  hmeofvalg  15529  bdmetval  15726  plycn  15988  mul2sq  16440  dichmul0orlem7  16964