Theorem oveq12 5827

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1335  (class class class)co 5818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-iota 5132  df-fv 5175  df-ov 5821

This theorem is referenced by:  oveq12i  5830  oveq12d  5836  oveqan12d  5837  ecopoveq  6568  ecopovtrn  6570  ecopovtrng  6573  th3qlem1  6575  th3qlem2  6576  mulcmpblnq  7271  addpipqqs  7273  ordpipqqs  7277  enq0breq  7339  mulcmpblnq0  7347  nqpnq0nq  7356  nqnq0a  7357  nqnq0m  7358  nq0m0r  7359  nq0a0  7360  distrlem5prl  7489  distrlem5pru  7490  addcmpblnr  7642  ltsrprg  7650  mulgt0sr  7681  add20  8332  cru  8460  qaddcl  9526  qmulcl  9528  xaddval  9731  xnn0xadd0  9753  fzopth  9945  modqval  10205  seqvalcd  10340  seqovcd  10344  1exp  10430  m1expeven  10448  nn0opthd  10578  faclbnd  10597  faclbnd3  10599  bcn0  10611  reval  10731  absval  10883  clim  11160  fsumparts  11349  dvds2add  11702  dvds2sub  11703  opoe  11767  omoe  11768  opeo  11769  omeo  11770  gcddvds  11827  gcdcl  11830  gcdeq0  11841  gcdneg  11846  gcdaddm  11848  gcdabs  11852  gcddiv  11883  eucalgval2  11910  lcmabs  11933  rpmul  11955  divgcdcoprmex  11959  prmexpb  12005  rpexp  12007  nn0gcdsq  12054  cnmpt2t  12653  cnmpt22f  12655  hmeofvalg  12663  bdmetval  12860