Theorem oveq12 5953

Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)

Assertion

Ref	Expression
oveq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12

Step	Hyp	Ref	Expression
1		oveq1 5951	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2		oveq2 5952	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
3	1, 2	sylan9eq 2258	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373  (class class class)co 5944

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 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  oveq12i  5956  oveq12d  5962  oveqan12d  5963  ecopoveq  6717  ecopovtrn  6719  ecopovtrng  6722  th3qlem1  6724  th3qlem2  6725  mulcmpblnq  7481  addpipqqs  7483  ordpipqqs  7487  enq0breq  7549  mulcmpblnq0  7557  nqpnq0nq  7566  nqnq0a  7567  nqnq0m  7568  nq0m0r  7569  nq0a0  7570  distrlem5prl  7699  distrlem5pru  7700  addcmpblnr  7852  ltsrprg  7860  mulgt0sr  7891  add20  8547  cru  8675  qaddcl  9756  qmulcl  9758  xaddval  9967  xnn0xadd0  9989  fzopth  10183  modqval  10469  seqvalcd  10606  seqovcd  10612  1exp  10713  m1expeven  10731  nn0opthd  10867  faclbnd  10886  faclbnd3  10888  bcn0  10900  reval  11160  absval  11312  clim  11592  fsumparts  11781  dvds2add  12136  dvds2sub  12137  opoe  12206  omoe  12207  opeo  12208  omeo  12209  gcddvds  12284  gcdcl  12287  gcdeq0  12298  gcdneg  12303  gcdaddm  12305  gcdabs  12309  gcddiv  12340  eucalgval2  12375  lcmabs  12398  rpmul  12420  divgcdcoprmex  12424  prmexpb  12473  rpexp  12475  nn0gcdsq  12522  pcqmul  12626  mul4sq  12717  f1ocpbl  13143  plusfvalg  13195  0subm  13316  imasabl  13672  ringadd2  13789  dfrhm2  13916  isrhm  13920  isrim0  13923  rhmval  13935  aprval  14044  scafvalg  14069  rmodislmodlem  14112  rmodislmod  14113  lss1d  14145  znidom  14419  mplvalcoe  14452  cnmpt2t  14765  cnmpt22f  14767  hmeofvalg  14775  bdmetval  14972  plycn  15234  mul2sq  15593