Theorem oveq12 5934

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

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

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 5928

This theorem is referenced by:  oveq12i  5937  oveq12d  5943  oveqan12d  5944  ecopoveq  6698  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  th3qlem2  6706  mulcmpblnq  7452  addpipqqs  7454  ordpipqqs  7458  enq0breq  7520  mulcmpblnq0  7528  nqpnq0nq  7537  nqnq0a  7538  nqnq0m  7539  nq0m0r  7540  nq0a0  7541  distrlem5prl  7670  distrlem5pru  7671  addcmpblnr  7823  ltsrprg  7831  mulgt0sr  7862  add20  8518  cru  8646  qaddcl  9726  qmulcl  9728  xaddval  9937  xnn0xadd0  9959  fzopth  10153  modqval  10433  seqvalcd  10570  seqovcd  10576  1exp  10677  m1expeven  10695  nn0opthd  10831  faclbnd  10850  faclbnd3  10852  bcn0  10864  reval  11031  absval  11183  clim  11463  fsumparts  11652  dvds2add  12007  dvds2sub  12008  opoe  12077  omoe  12078  opeo  12079  omeo  12080  gcddvds  12155  gcdcl  12158  gcdeq0  12169  gcdneg  12174  gcdaddm  12176  gcdabs  12180  gcddiv  12211  eucalgval2  12246  lcmabs  12269  rpmul  12291  divgcdcoprmex  12295  prmexpb  12344  rpexp  12346  nn0gcdsq  12393  pcqmul  12497  mul4sq  12588  f1ocpbl  13013  plusfvalg  13065  0subm  13186  imasabl  13542  ringadd2  13659  dfrhm2  13786  isrhm  13790  isrim0  13793  rhmval  13805  aprval  13914  scafvalg  13939  rmodislmodlem  13982  rmodislmod  13983  lss1d  14015  znidom  14289  cnmpt2t  14613  cnmpt22f  14615  hmeofvalg  14623  bdmetval  14820  plycn  15082  mul2sq  15441