Theorem oveq12i 6070

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

Syntax hints:   = wceq 1398  (class class class)co 6058

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  oveq123i  6072  1lt2nq  7737  halfnqq  7741  caucvgprprlemnbj  8024  caucvgprprlemaddq  8039  m1p1sr  8091  m1m1sr  8092  axi2m1  8206  negdii  8573  3t3e9  9412  8th4div3  9474  halfpm6th  9475  numma  9770  decmul10add  9795  4t3lem  9823  9t11e99  9856  halfthird  9869  5recm6rec  9870  fz0to3un2pr  10479  sqdivapi  11009  sq4e2t8  11023  i4  11028  binom2i  11034  facp1  11117  fac2  11118  fac3  11119  fac4  11120  4bc2eq6  11162  cji  11612  fsumadd  12117  fsumsplitf  12119  fsumsplitsnun  12130  0.999...  12232  fprodmul  12302  fprodsplitf  12343  ef01bndlem  12467  cos2bnd  12471  3dvds2dec  12577  flodddiv4  12647  nn0gcdsq  12922  pythagtriplem16  13002  4sqlem19  13132  dec5nprm  13137  dec2nprm  13138  numexp2x  13148  decsplit  13152  karatsuba  13153  2exp5  13155  2exp11  13159  2exp16  13160  ballotfilem2  13172  ballotfilemfval0  13179  ballotfilemth  13225  ecqusaddd  13991  isrhm  14403  cnmpt2res  15288  txmetcnp  15509  dveflem  15717  efhalfpi  15790  efipi  15792  sin2pi  15794  ef2pi  15796  sincosq3sgn  15819  sincosq4sgn  15820  sinq34lt0t  15822  sincos4thpi  15831  tan4thpi  15832  sincos6thpi  15833  sincos3rdpi  15834  pigt3  15835  1sgm2ppw  15989  lgsdi  16036  lgsquadlem1  16076  2lgsoddprmlem3c  16108  2lgsoddprmlem3d  16109  ex-exp  16621  ex-fac  16622  ex-bc  16623