Theorem oveq12 5866

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

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

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 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-rex 2455  df-v 2733  df-un 3126  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-iota 5162  df-fv 5208  df-ov 5860

This theorem is referenced by:  oveq12i  5869  oveq12d  5875  oveqan12d  5876  ecopoveq  6612  ecopovtrn  6614  ecopovtrng  6617  th3qlem1  6619  th3qlem2  6620  mulcmpblnq  7334  addpipqqs  7336  ordpipqqs  7340  enq0breq  7402  mulcmpblnq0  7410  nqpnq0nq  7419  nqnq0a  7420  nqnq0m  7421  nq0m0r  7422  nq0a0  7423  distrlem5prl  7552  distrlem5pru  7553  addcmpblnr  7705  ltsrprg  7713  mulgt0sr  7744  add20  8397  cru  8525  qaddcl  9598  qmulcl  9600  xaddval  9806  xnn0xadd0  9828  fzopth  10021  modqval  10284  seqvalcd  10419  seqovcd  10423  1exp  10509  m1expeven  10527  nn0opthd  10660  faclbnd  10679  faclbnd3  10681  bcn0  10693  reval  10817  absval  10969  clim  11248  fsumparts  11437  dvds2add  11791  dvds2sub  11792  opoe  11858  omoe  11859  opeo  11860  omeo  11861  gcddvds  11922  gcdcl  11925  gcdeq0  11936  gcdneg  11941  gcdaddm  11943  gcdabs  11947  gcddiv  11978  eucalgval2  12011  lcmabs  12034  rpmul  12056  divgcdcoprmex  12060  prmexpb  12109  rpexp  12111  nn0gcdsq  12158  pcqmul  12261  mul4sq  12350  plusfvalg  12621  0subm  12706  cnmpt2t  13172  cnmpt22f  13174  hmeofvalg  13182  bdmetval  13379  mul2sq  13831