Theorem oveq12 6097

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402  (class class class)co 6088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  oveq12i  6100  oveq12d  6106  oveqan12d  6107  ecopoveq  6909  ecopovtrn  6911  ecopovtrng  6914  th3qlem1  6916  th3qlem2  6917  mulcmpblnq  7741  addpipqqs  7743  ordpipqqs  7747  enq0breq  7809  mulcmpblnq0  7817  nqpnq0nq  7826  nqnq0a  7827  nqnq0m  7828  nq0m0r  7829  nq0a0  7830  distrlem5prl  7959  distrlem5pru  7960  addcmpblnr  8112  ltsrprg  8120  mulgt0sr  8151  add20  8809  cru  8938  qaddcl  10050  qmulcl  10052  xaddval  10263  xnn0xadd0  10285  fzopth  10483  modqval  10781  seqvalcd  10918  seqovcd  10924  1exp  11025  m1expeven  11043  nn0opthd  11181  faclbnd  11200  faclbnd3  11202  bcn0  11214  ccatopth  11509  ccatopth2  11510  reval  11635  absval  11788  clim  12071  fsumparts  12261  dvds2add  12616  dvds2sub  12617  opoe  12686  omoe  12687  opeo  12688  omeo  12689  gcddvds  12764  gcdcl  12767  gcdeq0  12778  gcdneg  12783  gcdaddm  12785  gcdabs  12789  gcddiv  12820  eucalgval2  12855  lcmabs  12878  rpmul  12900  divgcdcoprmex  12904  prmexpb  12954  rpexp  12956  nn0gcdsq  13004  pcqmul  13110  mul4sq  13201  f1ocpbl  13690  plusfvalg  13741  0subm  13849  imasabl  14229  ringadd2  14438  dfrhm2  14569  isrhm  14573  isrim0  14576  rhmval  14588  aprval  14699  scafvalg  14752  rmodislmodlem  14795  rmodislmod  14796  lss1d  14828  znidom  15100  mplvalg  15222  cnmpt2t  15536  cnmpt22f  15538  hmeofvalg  15546  bdmetval  15743  plycn  16005  mul2sq  16457  dichmul0orlem7  16981