Theorem oveq12 5862

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 5860	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2		oveq2 5861	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
3	1, 2	sylan9eq 2223	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1348  (class class class)co 5853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856

This theorem is referenced by:  oveq12i  5865  oveq12d  5871  oveqan12d  5872  ecopoveq  6608  ecopovtrn  6610  ecopovtrng  6613  th3qlem1  6615  th3qlem2  6616  mulcmpblnq  7330  addpipqqs  7332  ordpipqqs  7336  enq0breq  7398  mulcmpblnq0  7406  nqpnq0nq  7415  nqnq0a  7416  nqnq0m  7417  nq0m0r  7418  nq0a0  7419  distrlem5prl  7548  distrlem5pru  7549  addcmpblnr  7701  ltsrprg  7709  mulgt0sr  7740  add20  8393  cru  8521  qaddcl  9594  qmulcl  9596  xaddval  9802  xnn0xadd0  9824  fzopth  10017  modqval  10280  seqvalcd  10415  seqovcd  10419  1exp  10505  m1expeven  10523  nn0opthd  10656  faclbnd  10675  faclbnd3  10677  bcn0  10689  reval  10813  absval  10965  clim  11244  fsumparts  11433  dvds2add  11787  dvds2sub  11788  opoe  11854  omoe  11855  opeo  11856  omeo  11857  gcddvds  11918  gcdcl  11921  gcdeq0  11932  gcdneg  11937  gcdaddm  11939  gcdabs  11943  gcddiv  11974  eucalgval2  12007  lcmabs  12030  rpmul  12052  divgcdcoprmex  12056  prmexpb  12105  rpexp  12107  nn0gcdsq  12154  pcqmul  12257  mul4sq  12346  plusfvalg  12617  0subm  12702  cnmpt2t  13087  cnmpt22f  13089  hmeofvalg  13097  bdmetval  13294  mul2sq  13746