Theorem oveq12 6037

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  oveq12i  6040  oveq12d  6046  oveqan12d  6047  ecopoveq  6842  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  th3qlem2  6850  isfsupp  7214  mulcmpblnq  7648  addpipqqs  7650  ordpipqqs  7654  enq0breq  7716  mulcmpblnq0  7724  nqpnq0nq  7733  nqnq0a  7734  nqnq0m  7735  nq0m0r  7736  nq0a0  7737  distrlem5prl  7866  distrlem5pru  7867  addcmpblnr  8019  ltsrprg  8027  mulgt0sr  8058  add20  8713  cru  8841  qaddcl  9930  qmulcl  9932  xaddval  10141  xnn0xadd0  10163  fzopth  10358  modqval  10649  seqvalcd  10786  seqovcd  10792  1exp  10893  m1expeven  10911  nn0opthd  11047  faclbnd  11066  faclbnd3  11068  bcn0  11080  ccatopth  11363  ccatopth2  11364  reval  11489  absval  11641  clim  11921  fsumparts  12111  dvds2add  12466  dvds2sub  12467  opoe  12536  omoe  12537  opeo  12538  omeo  12539  gcddvds  12614  gcdcl  12617  gcdeq0  12628  gcdneg  12633  gcdaddm  12635  gcdabs  12639  gcddiv  12670  eucalgval2  12705  lcmabs  12728  rpmul  12750  divgcdcoprmex  12754  prmexpb  12803  rpexp  12805  nn0gcdsq  12852  pcqmul  12956  mul4sq  13047  f1ocpbl  13474  plusfvalg  13526  0subm  13647  imasabl  14003  ringadd2  14121  dfrhm2  14249  isrhm  14253  isrim0  14256  rhmval  14268  aprval  14378  scafvalg  14403  rmodislmodlem  14446  rmodislmod  14447  lss1d  14479  znidom  14753  mplvalcoe  14791  cnmpt2t  15104  cnmpt22f  15106  hmeofvalg  15114  bdmetval  15311  plycn  15573  mul2sq  15935