Theorem oveq12 5928

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

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

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  oveq12i  5931  oveq12d  5937  oveqan12d  5938  ecopoveq  6686  ecopovtrn  6688  ecopovtrng  6691  th3qlem1  6693  th3qlem2  6694  mulcmpblnq  7430  addpipqqs  7432  ordpipqqs  7436  enq0breq  7498  mulcmpblnq0  7506  nqpnq0nq  7515  nqnq0a  7516  nqnq0m  7517  nq0m0r  7518  nq0a0  7519  distrlem5prl  7648  distrlem5pru  7649  addcmpblnr  7801  ltsrprg  7809  mulgt0sr  7840  add20  8495  cru  8623  qaddcl  9703  qmulcl  9705  xaddval  9914  xnn0xadd0  9936  fzopth  10130  modqval  10398  seqvalcd  10535  seqovcd  10541  1exp  10642  m1expeven  10660  nn0opthd  10796  faclbnd  10815  faclbnd3  10817  bcn0  10829  reval  10996  absval  11148  clim  11427  fsumparts  11616  dvds2add  11971  dvds2sub  11972  opoe  12039  omoe  12040  opeo  12041  omeo  12042  gcddvds  12103  gcdcl  12106  gcdeq0  12117  gcdneg  12122  gcdaddm  12124  gcdabs  12128  gcddiv  12159  eucalgval2  12194  lcmabs  12217  rpmul  12239  divgcdcoprmex  12243  prmexpb  12292  rpexp  12294  nn0gcdsq  12341  pcqmul  12444  mul4sq  12535  f1ocpbl  12897  plusfvalg  12949  0subm  13059  imasabl  13409  ringadd2  13526  dfrhm2  13653  isrhm  13657  isrim0  13660  rhmval  13672  aprval  13781  scafvalg  13806  rmodislmodlem  13849  rmodislmod  13850  lss1d  13882  znidom  14156  cnmpt2t  14472  cnmpt22f  14474  hmeofvalg  14482  bdmetval  14679  plycn  14940  mul2sq  15273