Theorem oveq12i 6062

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053

This theorem is referenced by:  oveq123i  6064  1lt2nq  7721  halfnqq  7725  caucvgprprlemnbj  8008  caucvgprprlemaddq  8023  m1p1sr  8075  m1m1sr  8076  axi2m1  8190  negdii  8557  3t3e9  9395  8th4div3  9457  halfpm6th  9458  numma  9752  decmul10add  9777  4t3lem  9805  9t11e99  9838  halfthird  9851  5recm6rec  9852  fz0to3un2pr  10457  sqdivapi  10985  sq4e2t8  10999  i4  11004  binom2i  11010  facp1  11092  fac2  11093  fac3  11094  fac4  11095  4bc2eq6  11137  cji  11587  fsumadd  12092  fsumsplitf  12094  fsumsplitsnun  12105  0.999...  12207  fprodmul  12277  fprodsplitf  12318  ef01bndlem  12442  cos2bnd  12446  3dvds2dec  12552  flodddiv4  12622  nn0gcdsq  12897  pythagtriplem16  12977  4sqlem19  13107  dec5nprm  13112  dec2nprm  13113  numexp2x  13123  decsplit  13127  karatsuba  13128  2exp5  13130  2exp11  13134  2exp16  13135  ballotfilem2  13142  ecqusaddd  13955  isrhm  14303  cnmpt2res  15162  txmetcnp  15383  dveflem  15591  efhalfpi  15664  efipi  15666  sin2pi  15668  ef2pi  15670  sincosq3sgn  15693  sincosq4sgn  15694  sinq34lt0t  15696  sincos4thpi  15705  tan4thpi  15706  sincos6thpi  15707  sincos3rdpi  15708  pigt3  15709  1sgm2ppw  15863  lgsdi  15910  lgsquadlem1  15950  2lgsoddprmlem3c  15982  2lgsoddprmlem3d  15983  ex-exp  16495  ex-fac  16496  ex-bc  16497