Theorem oveq12i 5931

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

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

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 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  oveq123i  5933  1lt2nq  7468  halfnqq  7472  caucvgprprlemnbj  7755  caucvgprprlemaddq  7770  m1p1sr  7822  m1m1sr  7823  axi2m1  7937  negdii  8305  3t3e9  9142  8th4div3  9204  halfpm6th  9205  numma  9494  decmul10add  9519  4t3lem  9547  9t11e99  9580  halfthird  9593  5recm6rec  9594  fz0to3un2pr  10192  sqdivapi  10697  sq4e2t8  10711  i4  10716  binom2i  10722  facp1  10804  fac2  10805  fac3  10806  fac4  10807  4bc2eq6  10848  cji  11049  fsumadd  11552  fsumsplitf  11554  fsumsplitsnun  11565  0.999...  11667  fprodmul  11737  fprodsplitf  11778  ef01bndlem  11902  cos2bnd  11906  3dvds2dec  12010  flodddiv4  12078  nn0gcdsq  12341  pythagtriplem16  12420  4sqlem19  12550  ecqusaddd  13311  isrhm  13657  cnmpt2res  14476  txmetcnp  14697  dveflem  14905  efhalfpi  14975  efipi  14977  sin2pi  14979  ef2pi  14981  sincosq3sgn  15004  sincosq4sgn  15005  sinq34lt0t  15007  sincos4thpi  15016  tan4thpi  15017  sincos6thpi  15018  sincos3rdpi  15019  pigt3  15020  lgsdi  15194  lgsquadlem1  15234  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  ex-exp  15289  ex-fac  15290  ex-bc  15291