Theorem oveq12i 5886

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

Syntax hints:   = wceq 1353  (class class class)co 5874

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  oveq123i  5888  1lt2nq  7404  halfnqq  7408  caucvgprprlemnbj  7691  caucvgprprlemaddq  7706  m1p1sr  7758  m1m1sr  7759  axi2m1  7873  negdii  8240  3t3e9  9075  8th4div3  9137  halfpm6th  9138  numma  9426  decmul10add  9451  4t3lem  9479  9t11e99  9512  halfthird  9525  5recm6rec  9526  fz0to3un2pr  10122  sqdivapi  10603  sq4e2t8  10617  i4  10622  binom2i  10628  facp1  10709  fac2  10710  fac3  10711  fac4  10712  4bc2eq6  10753  cji  10910  fsumadd  11413  fsumsplitf  11415  fsumsplitsnun  11426  0.999...  11528  fprodmul  11598  fprodsplitf  11639  ef01bndlem  11763  cos2bnd  11767  3dvds2dec  11870  flodddiv4  11938  nn0gcdsq  12199  pythagtriplem16  12278  cnmpt2res  13767  txmetcnp  13988  dveflem  14157  efhalfpi  14190  efipi  14192  sin2pi  14194  ef2pi  14196  sincosq3sgn  14219  sincosq4sgn  14220  sinq34lt0t  14222  sincos4thpi  14231  tan4thpi  14232  sincos6thpi  14233  sincos3rdpi  14234  pigt3  14235  lgsdi  14408  2lgsoddprmlem3c  14427  2lgsoddprmlem3d  14428  ex-exp  14449  ex-fac  14450  ex-bc  14451