Theorem oveq12 5791

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332  (class class class)co 5782

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  oveq12i  5794  oveq12d  5800  oveqan12d  5801  ecopoveq  6532  ecopovtrn  6534  ecopovtrng  6537  th3qlem1  6539  th3qlem2  6540  mulcmpblnq  7200  addpipqqs  7202  ordpipqqs  7206  enq0breq  7268  mulcmpblnq0  7276  nqpnq0nq  7285  nqnq0a  7286  nqnq0m  7287  nq0m0r  7288  nq0a0  7289  distrlem5prl  7418  distrlem5pru  7419  addcmpblnr  7571  ltsrprg  7579  mulgt0sr  7610  add20  8260  cru  8388  qaddcl  9454  qmulcl  9456  xaddval  9658  xnn0xadd0  9680  fzopth  9872  modqval  10128  seqvalcd  10263  seqovcd  10267  1exp  10353  m1expeven  10371  nn0opthd  10500  faclbnd  10519  faclbnd3  10521  bcn0  10533  reval  10653  absval  10805  clim  11082  fsumparts  11271  dvds2add  11563  dvds2sub  11564  opoe  11628  omoe  11629  opeo  11630  omeo  11631  gcddvds  11688  gcdcl  11691  gcdeq0  11701  gcdneg  11706  gcdaddm  11708  gcdabs  11712  gcddiv  11743  eucalgval2  11770  lcmabs  11793  rpmul  11815  divgcdcoprmex  11819  prmexpb  11865  rpexp  11867  nn0gcdsq  11914  cnmpt2t  12501  cnmpt22f  12503  hmeofvalg  12511  bdmetval  12708