Theorem oveq12 5900

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364  (class class class)co 5891

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 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5193  df-fv 5239  df-ov 5894

This theorem is referenced by:  oveq12i  5903  oveq12d  5909  oveqan12d  5910  ecopoveq  6648  ecopovtrn  6650  ecopovtrng  6653  th3qlem1  6655  th3qlem2  6656  mulcmpblnq  7385  addpipqqs  7387  ordpipqqs  7391  enq0breq  7453  mulcmpblnq0  7461  nqpnq0nq  7470  nqnq0a  7471  nqnq0m  7472  nq0m0r  7473  nq0a0  7474  distrlem5prl  7603  distrlem5pru  7604  addcmpblnr  7756  ltsrprg  7764  mulgt0sr  7795  add20  8449  cru  8577  qaddcl  9653  qmulcl  9655  xaddval  9863  xnn0xadd0  9885  fzopth  10079  modqval  10342  seqvalcd  10477  seqovcd  10481  1exp  10567  m1expeven  10585  nn0opthd  10720  faclbnd  10739  faclbnd3  10741  bcn0  10753  reval  10876  absval  11028  clim  11307  fsumparts  11496  dvds2add  11850  dvds2sub  11851  opoe  11918  omoe  11919  opeo  11920  omeo  11921  gcddvds  11982  gcdcl  11985  gcdeq0  11996  gcdneg  12001  gcdaddm  12003  gcdabs  12007  gcddiv  12038  eucalgval2  12071  lcmabs  12094  rpmul  12116  divgcdcoprmex  12120  prmexpb  12169  rpexp  12171  nn0gcdsq  12218  pcqmul  12321  mul4sq  12410  f1ocpbl  12754  plusfvalg  12805  0subm  12902  imasabl  13234  ringadd2  13342  dfrhm2  13465  isrhm  13469  isrim0  13472  rhmval  13484  aprval  13559  scafvalg  13584  rmodislmodlem  13627  rmodislmod  13628  lss1d  13660  cnmpt2t  14190  cnmpt22f  14192  hmeofvalg  14200  bdmetval  14397  mul2sq  14860