Theorem oveq12 6027

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  oveq12i  6030  oveq12d  6036  oveqan12d  6037  ecopoveq  6799  ecopovtrn  6801  ecopovtrng  6804  th3qlem1  6806  th3qlem2  6807  mulcmpblnq  7588  addpipqqs  7590  ordpipqqs  7594  enq0breq  7656  mulcmpblnq0  7664  nqpnq0nq  7673  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  nq0a0  7677  distrlem5prl  7806  distrlem5pru  7807  addcmpblnr  7959  ltsrprg  7967  mulgt0sr  7998  add20  8654  cru  8782  qaddcl  9869  qmulcl  9871  xaddval  10080  xnn0xadd0  10102  fzopth  10296  modqval  10587  seqvalcd  10724  seqovcd  10730  1exp  10831  m1expeven  10849  nn0opthd  10985  faclbnd  11004  faclbnd3  11006  bcn0  11018  ccatopth  11298  ccatopth2  11299  reval  11411  absval  11563  clim  11843  fsumparts  12033  dvds2add  12388  dvds2sub  12389  opoe  12458  omoe  12459  opeo  12460  omeo  12461  gcddvds  12536  gcdcl  12539  gcdeq0  12550  gcdneg  12555  gcdaddm  12557  gcdabs  12561  gcddiv  12592  eucalgval2  12627  lcmabs  12650  rpmul  12672  divgcdcoprmex  12676  prmexpb  12725  rpexp  12727  nn0gcdsq  12774  pcqmul  12878  mul4sq  12969  f1ocpbl  13396  plusfvalg  13448  0subm  13569  imasabl  13925  ringadd2  14043  dfrhm2  14171  isrhm  14175  isrim0  14178  rhmval  14190  aprval  14299  scafvalg  14324  rmodislmodlem  14367  rmodislmod  14368  lss1d  14400  znidom  14674  mplvalcoe  14707  cnmpt2t  15020  cnmpt22f  15022  hmeofvalg  15030  bdmetval  15227  plycn  15489  mul2sq  15848