Theorem oveq12 5859

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

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

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 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5853

This theorem is referenced by:  oveq12i  5862  oveq12d  5868  oveqan12d  5869  ecopoveq  6604  ecopovtrn  6606  ecopovtrng  6609  th3qlem1  6611  th3qlem2  6612  mulcmpblnq  7317  addpipqqs  7319  ordpipqqs  7323  enq0breq  7385  mulcmpblnq0  7393  nqpnq0nq  7402  nqnq0a  7403  nqnq0m  7404  nq0m0r  7405  nq0a0  7406  distrlem5prl  7535  distrlem5pru  7536  addcmpblnr  7688  ltsrprg  7696  mulgt0sr  7727  add20  8380  cru  8508  qaddcl  9581  qmulcl  9583  xaddval  9789  xnn0xadd0  9811  fzopth  10004  modqval  10267  seqvalcd  10402  seqovcd  10406  1exp  10492  m1expeven  10510  nn0opthd  10643  faclbnd  10662  faclbnd3  10664  bcn0  10676  reval  10800  absval  10952  clim  11231  fsumparts  11420  dvds2add  11774  dvds2sub  11775  opoe  11841  omoe  11842  opeo  11843  omeo  11844  gcddvds  11905  gcdcl  11908  gcdeq0  11919  gcdneg  11924  gcdaddm  11926  gcdabs  11930  gcddiv  11961  eucalgval2  11994  lcmabs  12017  rpmul  12039  divgcdcoprmex  12043  prmexpb  12092  rpexp  12094  nn0gcdsq  12141  pcqmul  12244  mul4sq  12333  plusfvalg  12604  0subm  12689  cnmpt2t  13046  cnmpt22f  13048  hmeofvalg  13056  bdmetval  13253  mul2sq  13705