Theorem oveq12 5955

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

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

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  oveq12i  5958  oveq12d  5964  oveqan12d  5965  ecopoveq  6719  ecopovtrn  6721  ecopovtrng  6724  th3qlem1  6726  th3qlem2  6727  mulcmpblnq  7483  addpipqqs  7485  ordpipqqs  7489  enq0breq  7551  mulcmpblnq0  7559  nqpnq0nq  7568  nqnq0a  7569  nqnq0m  7570  nq0m0r  7571  nq0a0  7572  distrlem5prl  7701  distrlem5pru  7702  addcmpblnr  7854  ltsrprg  7862  mulgt0sr  7893  add20  8549  cru  8677  qaddcl  9758  qmulcl  9760  xaddval  9969  xnn0xadd0  9991  fzopth  10185  modqval  10471  seqvalcd  10608  seqovcd  10614  1exp  10715  m1expeven  10733  nn0opthd  10869  faclbnd  10888  faclbnd3  10890  bcn0  10902  reval  11193  absval  11345  clim  11625  fsumparts  11814  dvds2add  12169  dvds2sub  12170  opoe  12239  omoe  12240  opeo  12241  omeo  12242  gcddvds  12317  gcdcl  12320  gcdeq0  12331  gcdneg  12336  gcdaddm  12338  gcdabs  12342  gcddiv  12373  eucalgval2  12408  lcmabs  12431  rpmul  12453  divgcdcoprmex  12457  prmexpb  12506  rpexp  12508  nn0gcdsq  12555  pcqmul  12659  mul4sq  12750  f1ocpbl  13176  plusfvalg  13228  0subm  13349  imasabl  13705  ringadd2  13822  dfrhm2  13949  isrhm  13953  isrim0  13956  rhmval  13968  aprval  14077  scafvalg  14102  rmodislmodlem  14145  rmodislmod  14146  lss1d  14178  znidom  14452  mplvalcoe  14485  cnmpt2t  14798  cnmpt22f  14800  hmeofvalg  14808  bdmetval  15005  plycn  15267  mul2sq  15626