Theorem oveq12i 5549

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

Syntax hints:   = wceq 1257  (class class class)co 5537

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036

This theorem depends on definitions:  df-bi 114  df-3an 896  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-rex 2327  df-v 2574  df-un 2947  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-br 3790  df-iota 4892  df-fv 4935  df-ov 5540

This theorem is referenced by:  oveq123i  5551  1lt2nq  6532  halfnqq  6536  caucvgprprlemnbj  6819  caucvgprprlemaddq  6834  m1p1sr  6873  m1m1sr  6874  axi2m1  6977  negdii  7328  3t3e9  8110  8th4div3  8171  halfpm6th  8172  numma  8440  decmul10add  8465  4t3lem  8493  9t11e99  8526  sqdivapi  9468  i4  9486  binom2i  9491  facp1  9562  fac2  9563  fac3  9564  fac4  9565  4bc2eq6  9606  cji  9694  3dvds2dec  10140  ex-fac  10224  ex-bc  10225