Theorem oveq12i 5718

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Hypotheses

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵
oveq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
oveq12i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Proof of Theorem oveq12i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		oveq12 5715	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	mp2an 420	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Syntax hints:   = wceq 1299  (class class class)co 5706

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-iota 5024  df-fv 5067  df-ov 5709

This theorem is referenced by:  oveq123i  5720  1lt2nq  7115  halfnqq  7119  caucvgprprlemnbj  7402  caucvgprprlemaddq  7417  m1p1sr  7456  m1m1sr  7457  axi2m1  7560  negdii  7917  3t3e9  8729  8th4div3  8791  halfpm6th  8792  numma  9077  decmul10add  9102  4t3lem  9130  9t11e99  9163  sqdivapi  10217  sq4e2t8  10231  i4  10236  binom2i  10242  facp1  10317  fac2  10318  fac3  10319  fac4  10320  4bc2eq6  10361  cji  10515  fsumadd  11014  fsumsplitf  11016  fsumsplitsnun  11027  0.999...  11129  ef01bndlem  11261  cos2bnd  11265  3dvds2dec  11358  flodddiv4  11426  nn0gcdsq  11670  cnmpt2res  12247  ex-exp  12542  ex-fac  12543  ex-bc  12544