Theorem oveq12 5976

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 5974	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
2		oveq2 5975	. 2 |- ( C = D -> ( B F C ) = ( B F D ) )
3	1, 2	sylan9eq 2260	1 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )

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

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  oveq12i  5979  oveq12d  5985  oveqan12d  5986  ecopoveq  6740  ecopovtrn  6742  ecopovtrng  6745  th3qlem1  6747  th3qlem2  6748  mulcmpblnq  7516  addpipqqs  7518  ordpipqqs  7522  enq0breq  7584  mulcmpblnq0  7592  nqpnq0nq  7601  nqnq0a  7602  nqnq0m  7603  nq0m0r  7604  nq0a0  7605  distrlem5prl  7734  distrlem5pru  7735  addcmpblnr  7887  ltsrprg  7895  mulgt0sr  7926  add20  8582  cru  8710  qaddcl  9791  qmulcl  9793  xaddval  10002  xnn0xadd0  10024  fzopth  10218  modqval  10506  seqvalcd  10643  seqovcd  10649  1exp  10750  m1expeven  10768  nn0opthd  10904  faclbnd  10923  faclbnd3  10925  bcn0  10937  ccatopth  11207  ccatopth2  11208  reval  11275  absval  11427  clim  11707  fsumparts  11896  dvds2add  12251  dvds2sub  12252  opoe  12321  omoe  12322  opeo  12323  omeo  12324  gcddvds  12399  gcdcl  12402  gcdeq0  12413  gcdneg  12418  gcdaddm  12420  gcdabs  12424  gcddiv  12455  eucalgval2  12490  lcmabs  12513  rpmul  12535  divgcdcoprmex  12539  prmexpb  12588  rpexp  12590  nn0gcdsq  12637  pcqmul  12741  mul4sq  12832  f1ocpbl  13258  plusfvalg  13310  0subm  13431  imasabl  13787  ringadd2  13904  dfrhm2  14031  isrhm  14035  isrim0  14038  rhmval  14050  aprval  14159  scafvalg  14184  rmodislmodlem  14227  rmodislmod  14228  lss1d  14260  znidom  14534  mplvalcoe  14567  cnmpt2t  14880  cnmpt22f  14882  hmeofvalg  14890  bdmetval  15087  plycn  15349  mul2sq  15708