Theorem oveq12i 5854

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 5851	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	mp2an 423	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Syntax hints:   = wceq 1343  (class class class)co 5842

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845

This theorem is referenced by:  oveq123i  5856  1lt2nq  7347  halfnqq  7351  caucvgprprlemnbj  7634  caucvgprprlemaddq  7649  m1p1sr  7701  m1m1sr  7702  axi2m1  7816  negdii  8182  3t3e9  9014  8th4div3  9076  halfpm6th  9077  numma  9365  decmul10add  9390  4t3lem  9418  9t11e99  9451  halfthird  9464  5recm6rec  9465  fz0to3un2pr  10058  sqdivapi  10538  sq4e2t8  10552  i4  10557  binom2i  10563  facp1  10643  fac2  10644  fac3  10645  fac4  10646  4bc2eq6  10687  cji  10844  fsumadd  11347  fsumsplitf  11349  fsumsplitsnun  11360  0.999...  11462  fprodmul  11532  fprodsplitf  11573  ef01bndlem  11697  cos2bnd  11701  3dvds2dec  11803  flodddiv4  11871  nn0gcdsq  12132  pythagtriplem16  12211  cnmpt2res  12937  txmetcnp  13158  dveflem  13327  efhalfpi  13360  efipi  13362  sin2pi  13364  ef2pi  13366  sincosq3sgn  13389  sincosq4sgn  13390  sinq34lt0t  13392  sincos4thpi  13401  tan4thpi  13402  sincos6thpi  13403  sincos3rdpi  13404  pigt3  13405  lgsdi  13578  ex-exp  13608  ex-fac  13609  ex-bc  13610