Theorem oveq12 5931

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

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

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 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  oveq12i  5934  oveq12d  5940  oveqan12d  5941  ecopoveq  6689  ecopovtrn  6691  ecopovtrng  6694  th3qlem1  6696  th3qlem2  6697  mulcmpblnq  7435  addpipqqs  7437  ordpipqqs  7441  enq0breq  7503  mulcmpblnq0  7511  nqpnq0nq  7520  nqnq0a  7521  nqnq0m  7522  nq0m0r  7523  nq0a0  7524  distrlem5prl  7653  distrlem5pru  7654  addcmpblnr  7806  ltsrprg  7814  mulgt0sr  7845  add20  8501  cru  8629  qaddcl  9709  qmulcl  9711  xaddval  9920  xnn0xadd0  9942  fzopth  10136  modqval  10416  seqvalcd  10553  seqovcd  10559  1exp  10660  m1expeven  10678  nn0opthd  10814  faclbnd  10833  faclbnd3  10835  bcn0  10847  reval  11014  absval  11166  clim  11446  fsumparts  11635  dvds2add  11990  dvds2sub  11991  opoe  12060  omoe  12061  opeo  12062  omeo  12063  gcddvds  12130  gcdcl  12133  gcdeq0  12144  gcdneg  12149  gcdaddm  12151  gcdabs  12155  gcddiv  12186  eucalgval2  12221  lcmabs  12244  rpmul  12266  divgcdcoprmex  12270  prmexpb  12319  rpexp  12321  nn0gcdsq  12368  pcqmul  12472  mul4sq  12563  f1ocpbl  12954  plusfvalg  13006  0subm  13116  imasabl  13466  ringadd2  13583  dfrhm2  13710  isrhm  13714  isrim0  13717  rhmval  13729  aprval  13838  scafvalg  13863  rmodislmodlem  13906  rmodislmod  13907  lss1d  13939  znidom  14213  cnmpt2t  14529  cnmpt22f  14531  hmeofvalg  14539  bdmetval  14736  plycn  14998  mul2sq  15357