Theorem oveq12 6084

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402  (class class class)co 6075

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 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 theorem 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 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078

This theorem is referenced by:  oveq12i  6087  oveq12d  6093  oveqan12d  6094  ecopoveq  6894  ecopovtrn  6896  ecopovtrng  6899  th3qlem1  6901  th3qlem2  6902  isfsupp  7279  mulcmpblnq  7725  addpipqqs  7727  ordpipqqs  7731  enq0breq  7793  mulcmpblnq0  7801  nqpnq0nq  7810  nqnq0a  7811  nqnq0m  7812  nq0m0r  7813  nq0a0  7814  distrlem5prl  7943  distrlem5pru  7944  addcmpblnr  8096  ltsrprg  8104  mulgt0sr  8135  add20  8792  cru  8920  qaddcl  10014  qmulcl  10016  xaddval  10226  xnn0xadd0  10248  fzopth  10445  modqval  10739  seqvalcd  10876  seqovcd  10882  1exp  10983  m1expeven  11001  nn0opthd  11138  faclbnd  11157  faclbnd3  11159  bcn0  11171  ccatopth  11466  ccatopth2  11467  reval  11592  absval  11745  clim  12025  fsumparts  12215  dvds2add  12570  dvds2sub  12571  opoe  12640  omoe  12641  opeo  12642  omeo  12643  gcddvds  12718  gcdcl  12721  gcdeq0  12732  gcdneg  12737  gcdaddm  12739  gcdabs  12743  gcddiv  12774  eucalgval2  12809  lcmabs  12832  rpmul  12854  divgcdcoprmex  12858  prmexpb  12907  rpexp  12909  nn0gcdsq  12956  pcqmul  13060  mul4sq  13151  f1ocpbl  13609  plusfvalg  13660  0subm  13768  imasabl  14117  ringadd2  14305  dfrhm2  14434  isrhm  14438  isrim0  14441  rhmval  14453  aprval  14564  scafvalg  14616  rmodislmodlem  14659  rmodislmod  14660  lss1d  14692  znidom  14964  mplvalcoe  15004  cnmpt2t  15317  cnmpt22f  15319  hmeofvalg  15327  bdmetval  15524  plycn  15786  mul2sq  16149  dichmul0orlem7  16673