Theorem oveq12i 6019

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

Syntax hints:   = wceq 1395  (class class class)co 6007

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  oveq123i  6021  1lt2nq  7604  halfnqq  7608  caucvgprprlemnbj  7891  caucvgprprlemaddq  7906  m1p1sr  7958  m1m1sr  7959  axi2m1  8073  negdii  8441  3t3e9  9279  8th4div3  9341  halfpm6th  9342  numma  9632  decmul10add  9657  4t3lem  9685  9t11e99  9718  halfthird  9731  5recm6rec  9732  fz0to3un2pr  10331  sqdivapi  10857  sq4e2t8  10871  i4  10876  binom2i  10882  facp1  10964  fac2  10965  fac3  10966  fac4  10967  4bc2eq6  11008  cji  11429  fsumadd  11933  fsumsplitf  11935  fsumsplitsnun  11946  0.999...  12048  fprodmul  12118  fprodsplitf  12159  ef01bndlem  12283  cos2bnd  12287  3dvds2dec  12393  flodddiv4  12463  nn0gcdsq  12738  pythagtriplem16  12818  4sqlem19  12948  dec5nprm  12953  dec2nprm  12954  numexp2x  12964  decsplit  12968  karatsuba  12969  2exp5  12971  2exp11  12975  2exp16  12976  ecqusaddd  13791  isrhm  14138  cnmpt2res  14987  txmetcnp  15208  dveflem  15416  efhalfpi  15489  efipi  15491  sin2pi  15493  ef2pi  15495  sincosq3sgn  15518  sincosq4sgn  15519  sinq34lt0t  15521  sincos4thpi  15530  tan4thpi  15531  sincos6thpi  15532  sincos3rdpi  15533  pigt3  15534  1sgm2ppw  15685  lgsdi  15732  lgsquadlem1  15772  2lgsoddprmlem3c  15804  2lgsoddprmlem3d  15805  ex-exp  16174  ex-fac  16175  ex-bc  16176