Theorem oveq12 6094

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

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

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 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq12i  6097  oveq12d  6103  oveqan12d  6104  ecopoveq  6904  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  th3qlem2  6912  isfsupp  7289  mulcmpblnq  7735  addpipqqs  7737  ordpipqqs  7741  enq0breq  7803  mulcmpblnq0  7811  nqpnq0nq  7820  nqnq0a  7821  nqnq0m  7822  nq0m0r  7823  nq0a0  7824  distrlem5prl  7953  distrlem5pru  7954  addcmpblnr  8106  ltsrprg  8114  mulgt0sr  8145  add20  8803  cru  8932  qaddcl  10044  qmulcl  10046  xaddval  10257  xnn0xadd0  10279  fzopth  10477  modqval  10774  seqvalcd  10911  seqovcd  10917  1exp  11018  m1expeven  11036  nn0opthd  11174  faclbnd  11193  faclbnd3  11195  bcn0  11207  ccatopth  11502  ccatopth2  11503  reval  11628  absval  11781  clim  12063  fsumparts  12253  dvds2add  12608  dvds2sub  12609  opoe  12678  omoe  12679  opeo  12680  omeo  12681  gcddvds  12756  gcdcl  12759  gcdeq0  12770  gcdneg  12775  gcdaddm  12777  gcdabs  12781  gcddiv  12812  eucalgval2  12847  lcmabs  12870  rpmul  12892  divgcdcoprmex  12896  prmexpb  12946  rpexp  12948  nn0gcdsq  12996  pcqmul  13102  mul4sq  13193  f1ocpbl  13681  plusfvalg  13732  0subm  13840  imasabl  14189  ringadd2  14381  dfrhm2  14510  isrhm  14514  isrim0  14517  rhmval  14529  aprval  14640  scafvalg  14693  rmodislmodlem  14736  rmodislmod  14737  lss1d  14769  znidom  15041  mplvalcoe  15130  cnmpt2t  15443  cnmpt22f  15445  hmeofvalg  15453  bdmetval  15650  plycn  15912  mul2sq  16333  dichmul0orlem7  16857