Theorem oveq12 5927

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 5925	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
2		oveq2 5926	. 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 5918

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 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  oveq12i  5930  oveq12d  5936  oveqan12d  5937  ecopoveq  6684  ecopovtrn  6686  ecopovtrng  6689  th3qlem1  6691  th3qlem2  6692  mulcmpblnq  7428  addpipqqs  7430  ordpipqqs  7434  enq0breq  7496  mulcmpblnq0  7504  nqpnq0nq  7513  nqnq0a  7514  nqnq0m  7515  nq0m0r  7516  nq0a0  7517  distrlem5prl  7646  distrlem5pru  7647  addcmpblnr  7799  ltsrprg  7807  mulgt0sr  7838  add20  8493  cru  8621  qaddcl  9700  qmulcl  9702  xaddval  9911  xnn0xadd0  9933  fzopth  10127  modqval  10395  seqvalcd  10532  seqovcd  10538  1exp  10639  m1expeven  10657  nn0opthd  10793  faclbnd  10812  faclbnd3  10814  bcn0  10826  reval  10993  absval  11145  clim  11424  fsumparts  11613  dvds2add  11968  dvds2sub  11969  opoe  12036  omoe  12037  opeo  12038  omeo  12039  gcddvds  12100  gcdcl  12103  gcdeq0  12114  gcdneg  12119  gcdaddm  12121  gcdabs  12125  gcddiv  12156  eucalgval2  12191  lcmabs  12214  rpmul  12236  divgcdcoprmex  12240  prmexpb  12289  rpexp  12291  nn0gcdsq  12338  pcqmul  12441  mul4sq  12532  f1ocpbl  12894  plusfvalg  12946  0subm  13056  imasabl  13406  ringadd2  13523  dfrhm2  13650  isrhm  13654  isrim0  13657  rhmval  13669  aprval  13778  scafvalg  13803  rmodislmodlem  13846  rmodislmod  13847  lss1d  13879  znidom  14145  cnmpt2t  14461  cnmpt22f  14463  hmeofvalg  14471  bdmetval  14668  mul2sq  15203