Theorem oveq12 5886

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

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

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880

This theorem is referenced by:  oveq12i  5889  oveq12d  5895  oveqan12d  5896  ecopoveq  6632  ecopovtrn  6634  ecopovtrng  6637  th3qlem1  6639  th3qlem2  6640  mulcmpblnq  7369  addpipqqs  7371  ordpipqqs  7375  enq0breq  7437  mulcmpblnq0  7445  nqpnq0nq  7454  nqnq0a  7455  nqnq0m  7456  nq0m0r  7457  nq0a0  7458  distrlem5prl  7587  distrlem5pru  7588  addcmpblnr  7740  ltsrprg  7748  mulgt0sr  7779  add20  8433  cru  8561  qaddcl  9637  qmulcl  9639  xaddval  9847  xnn0xadd0  9869  fzopth  10063  modqval  10326  seqvalcd  10461  seqovcd  10465  1exp  10551  m1expeven  10569  nn0opthd  10704  faclbnd  10723  faclbnd3  10725  bcn0  10737  reval  10860  absval  11012  clim  11291  fsumparts  11480  dvds2add  11834  dvds2sub  11835  opoe  11902  omoe  11903  opeo  11904  omeo  11905  gcddvds  11966  gcdcl  11969  gcdeq0  11980  gcdneg  11985  gcdaddm  11987  gcdabs  11991  gcddiv  12022  eucalgval2  12055  lcmabs  12078  rpmul  12100  divgcdcoprmex  12104  prmexpb  12153  rpexp  12155  nn0gcdsq  12202  pcqmul  12305  mul4sq  12394  f1ocpbl  12737  plusfvalg  12787  0subm  12876  ringadd2  13215  aprval  13377  scafvalg  13402  rmodislmodlem  13445  rmodislmod  13446  lss1d  13475  cnmpt2t  13878  cnmpt22f  13880  hmeofvalg  13888  bdmetval  14085  mul2sq  14548