Theorem oveq12 6027

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  oveq12i  6030  oveq12d  6036  oveqan12d  6037  ecopoveq  6799  ecopovtrn  6801  ecopovtrng  6804  th3qlem1  6806  th3qlem2  6807  mulcmpblnq  7588  addpipqqs  7590  ordpipqqs  7594  enq0breq  7656  mulcmpblnq0  7664  nqpnq0nq  7673  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  nq0a0  7677  distrlem5prl  7806  distrlem5pru  7807  addcmpblnr  7959  ltsrprg  7967  mulgt0sr  7998  add20  8654  cru  8782  qaddcl  9869  qmulcl  9871  xaddval  10080  xnn0xadd0  10102  fzopth  10296  modqval  10587  seqvalcd  10724  seqovcd  10730  1exp  10831  m1expeven  10849  nn0opthd  10985  faclbnd  11004  faclbnd3  11006  bcn0  11018  ccatopth  11301  ccatopth2  11302  reval  11427  absval  11579  clim  11859  fsumparts  12049  dvds2add  12404  dvds2sub  12405  opoe  12474  omoe  12475  opeo  12476  omeo  12477  gcddvds  12552  gcdcl  12555  gcdeq0  12566  gcdneg  12571  gcdaddm  12573  gcdabs  12577  gcddiv  12608  eucalgval2  12643  lcmabs  12666  rpmul  12688  divgcdcoprmex  12692  prmexpb  12741  rpexp  12743  nn0gcdsq  12790  pcqmul  12894  mul4sq  12985  f1ocpbl  13412  plusfvalg  13464  0subm  13585  imasabl  13941  ringadd2  14059  dfrhm2  14187  isrhm  14191  isrim0  14194  rhmval  14206  aprval  14315  scafvalg  14340  rmodislmodlem  14383  rmodislmod  14384  lss1d  14416  znidom  14690  mplvalcoe  14723  cnmpt2t  15036  cnmpt22f  15038  hmeofvalg  15046  bdmetval  15243  plycn  15505  mul2sq  15864