Theorem oveq12 5932

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364  (class class class)co 5923

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5926

This theorem is referenced by:  oveq12i  5935  oveq12d  5941  oveqan12d  5942  ecopoveq  6690  ecopovtrn  6692  ecopovtrng  6695  th3qlem1  6697  th3qlem2  6698  mulcmpblnq  7437  addpipqqs  7439  ordpipqqs  7443  enq0breq  7505  mulcmpblnq0  7513  nqpnq0nq  7522  nqnq0a  7523  nqnq0m  7524  nq0m0r  7525  nq0a0  7526  distrlem5prl  7655  distrlem5pru  7656  addcmpblnr  7808  ltsrprg  7816  mulgt0sr  7847  add20  8503  cru  8631  qaddcl  9711  qmulcl  9713  xaddval  9922  xnn0xadd0  9944  fzopth  10138  modqval  10418  seqvalcd  10555  seqovcd  10561  1exp  10662  m1expeven  10680  nn0opthd  10816  faclbnd  10835  faclbnd3  10837  bcn0  10849  reval  11016  absval  11168  clim  11448  fsumparts  11637  dvds2add  11992  dvds2sub  11993  opoe  12062  omoe  12063  opeo  12064  omeo  12065  gcddvds  12140  gcdcl  12143  gcdeq0  12154  gcdneg  12159  gcdaddm  12161  gcdabs  12165  gcddiv  12196  eucalgval2  12231  lcmabs  12254  rpmul  12276  divgcdcoprmex  12280  prmexpb  12329  rpexp  12331  nn0gcdsq  12378  pcqmul  12482  mul4sq  12573  f1ocpbl  12964  plusfvalg  13016  0subm  13126  imasabl  13476  ringadd2  13593  dfrhm2  13720  isrhm  13724  isrim0  13727  rhmval  13739  aprval  13848  scafvalg  13873  rmodislmodlem  13916  rmodislmod  13917  lss1d  13949  znidom  14223  cnmpt2t  14539  cnmpt22f  14541  hmeofvalg  14549  bdmetval  14746  plycn  15008  mul2sq  15367