Theorem oveq12i 5912

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

Syntax hints:   = wceq 1364  (class class class)co 5900

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-br 4022  df-iota 5199  df-fv 5246  df-ov 5903

This theorem is referenced by:  oveq123i  5914  1lt2nq  7440  halfnqq  7444  caucvgprprlemnbj  7727  caucvgprprlemaddq  7742  m1p1sr  7794  m1m1sr  7795  axi2m1  7909  negdii  8276  3t3e9  9111  8th4div3  9173  halfpm6th  9174  numma  9462  decmul10add  9487  4t3lem  9515  9t11e99  9548  halfthird  9561  5recm6rec  9562  fz0to3un2pr  10159  sqdivapi  10644  sq4e2t8  10658  i4  10663  binom2i  10669  facp1  10751  fac2  10752  fac3  10753  fac4  10754  4bc2eq6  10795  cji  10952  fsumadd  11455  fsumsplitf  11457  fsumsplitsnun  11468  0.999...  11570  fprodmul  11640  fprodsplitf  11681  ef01bndlem  11805  cos2bnd  11809  3dvds2dec  11912  flodddiv4  11980  nn0gcdsq  12243  pythagtriplem16  12322  4sqlem19  12452  ecqusaddd  13202  isrhm  13533  cnmpt2res  14282  txmetcnp  14503  dveflem  14672  efhalfpi  14705  efipi  14707  sin2pi  14709  ef2pi  14711  sincosq3sgn  14734  sincosq4sgn  14735  sinq34lt0t  14737  sincos4thpi  14746  tan4thpi  14747  sincos6thpi  14748  sincos3rdpi  14749  pigt3  14750  lgsdi  14924  2lgsoddprmlem3c  14943  2lgsoddprmlem3d  14944  ex-exp  14965  ex-fac  14966  ex-bc  14967