Theorem oveq12 6026

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 6024	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
2		oveq2 6025	. 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 1397  (class class class)co 6017

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  oveq12i  6029  oveq12d  6035  oveqan12d  6036  ecopoveq  6798  ecopovtrn  6800  ecopovtrng  6803  th3qlem1  6805  th3qlem2  6806  mulcmpblnq  7587  addpipqqs  7589  ordpipqqs  7593  enq0breq  7655  mulcmpblnq0  7663  nqpnq0nq  7672  nqnq0a  7673  nqnq0m  7674  nq0m0r  7675  nq0a0  7676  distrlem5prl  7805  distrlem5pru  7806  addcmpblnr  7958  ltsrprg  7966  mulgt0sr  7997  add20  8653  cru  8781  qaddcl  9868  qmulcl  9870  xaddval  10079  xnn0xadd0  10101  fzopth  10295  modqval  10585  seqvalcd  10722  seqovcd  10728  1exp  10829  m1expeven  10847  nn0opthd  10983  faclbnd  11002  faclbnd3  11004  bcn0  11016  ccatopth  11296  ccatopth2  11297  reval  11409  absval  11561  clim  11841  fsumparts  12030  dvds2add  12385  dvds2sub  12386  opoe  12455  omoe  12456  opeo  12457  omeo  12458  gcddvds  12533  gcdcl  12536  gcdeq0  12547  gcdneg  12552  gcdaddm  12554  gcdabs  12558  gcddiv  12589  eucalgval2  12624  lcmabs  12647  rpmul  12669  divgcdcoprmex  12673  prmexpb  12722  rpexp  12724  nn0gcdsq  12771  pcqmul  12875  mul4sq  12966  f1ocpbl  13393  plusfvalg  13445  0subm  13566  imasabl  13922  ringadd2  14039  dfrhm2  14167  isrhm  14171  isrim0  14174  rhmval  14186  aprval  14295  scafvalg  14320  rmodislmodlem  14363  rmodislmod  14364  lss1d  14396  znidom  14670  mplvalcoe  14703  cnmpt2t  15016  cnmpt22f  15018  hmeofvalg  15026  bdmetval  15223  plycn  15485  mul2sq  15844