Theorem oveq12 6037

Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)

Assertion

Ref	Expression
oveq12	|- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )

Proof of Theorem oveq12

Step	Hyp	Ref	Expression
1		oveq1 6035	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
2		oveq2 6036	. 2 |- ( C = D -> ( B F C ) = ( B F D ) )
3	1, 2	sylan9eq 2284	1 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398  (class class class)co 6028

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  oveq12i  6040  oveq12d  6046  oveqan12d  6047  ecopoveq  6842  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  th3qlem2  6850  mulcmpblnq  7631  addpipqqs  7633  ordpipqqs  7637  enq0breq  7699  mulcmpblnq0  7707  nqpnq0nq  7716  nqnq0a  7717  nqnq0m  7718  nq0m0r  7719  nq0a0  7720  distrlem5prl  7849  distrlem5pru  7850  addcmpblnr  8002  ltsrprg  8010  mulgt0sr  8041  add20  8696  cru  8824  qaddcl  9913  qmulcl  9915  xaddval  10124  xnn0xadd0  10146  fzopth  10341  modqval  10632  seqvalcd  10769  seqovcd  10775  1exp  10876  m1expeven  10894  nn0opthd  11030  faclbnd  11049  faclbnd3  11051  bcn0  11063  ccatopth  11346  ccatopth2  11347  reval  11472  absval  11624  clim  11904  fsumparts  12094  dvds2add  12449  dvds2sub  12450  opoe  12519  omoe  12520  opeo  12521  omeo  12522  gcddvds  12597  gcdcl  12600  gcdeq0  12611  gcdneg  12616  gcdaddm  12618  gcdabs  12622  gcddiv  12653  eucalgval2  12688  lcmabs  12711  rpmul  12733  divgcdcoprmex  12737  prmexpb  12786  rpexp  12788  nn0gcdsq  12835  pcqmul  12939  mul4sq  13030  f1ocpbl  13457  plusfvalg  13509  0subm  13630  imasabl  13986  ringadd2  14104  dfrhm2  14232  isrhm  14236  isrim0  14239  rhmval  14251  aprval  14361  scafvalg  14386  rmodislmodlem  14429  rmodislmod  14430  lss1d  14462  znidom  14736  mplvalcoe  14774  cnmpt2t  15087  cnmpt22f  15089  hmeofvalg  15097  bdmetval  15294  plycn  15556  mul2sq  15918