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  8802  cru  8930  qaddcl  10035  qmulcl  10037  xaddval  10247  xnn0xadd0  10269  fzopth  10467  modqval  10761  seqvalcd  10898  seqovcd  10904  1exp  11005  m1expeven  11023  nn0opthd  11160  faclbnd  11179  faclbnd3  11181  bcn0  11193  ccatopth  11488  ccatopth2  11489  reval  11614  absval  11767  clim  12047  fsumparts  12237  dvds2add  12592  dvds2sub  12593  opoe  12662  omoe  12663  opeo  12664  omeo  12665  gcddvds  12740  gcdcl  12743  gcdeq0  12754  gcdneg  12759  gcdaddm  12761  gcdabs  12765  gcddiv  12796  eucalgval2  12831  lcmabs  12854  rpmul  12876  divgcdcoprmex  12880  prmexpb  12929  rpexp  12931  nn0gcdsq  12978  pcqmul  13082  mul4sq  13173  f1ocpbl  13632  plusfvalg  13683  0subm  13791  imasabl  14140  ringadd2  14332  dfrhm2  14461  isrhm  14465  isrim0  14468  rhmval  14480  aprval  14591  scafvalg  14644  rmodislmodlem  14687  rmodislmod  14688  lss1d  14720  znidom  14992  mplvalcoe  15081  cnmpt2t  15394  cnmpt22f  15396  hmeofvalg  15404  bdmetval  15601  plycn  15863  mul2sq  16235  dichmul0orlem7  16759