ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq12i GIF version

Theorem oveq12i 5754
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
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq12i.2 . 2 𝐶 = 𝐷
3 oveq12 5751 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3mp2an 422 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Colors of variables: wff set class
Syntax hints:   = wceq 1316  (class class class)co 5742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101  df-ov 5745
This theorem is referenced by:  oveq123i  5756  1lt2nq  7182  halfnqq  7186  caucvgprprlemnbj  7469  caucvgprprlemaddq  7484  m1p1sr  7536  m1m1sr  7537  axi2m1  7651  negdii  8014  3t3e9  8845  8th4div3  8907  halfpm6th  8908  numma  9193  decmul10add  9218  4t3lem  9246  9t11e99  9279  halfthird  9292  5recm6rec  9293  sqdivapi  10344  sq4e2t8  10358  i4  10363  binom2i  10369  facp1  10444  fac2  10445  fac3  10446  fac4  10447  4bc2eq6  10488  cji  10642  fsumadd  11143  fsumsplitf  11145  fsumsplitsnun  11156  0.999...  11258  ef01bndlem  11390  cos2bnd  11394  3dvds2dec  11490  flodddiv4  11558  nn0gcdsq  11805  cnmpt2res  12393  txmetcnp  12614  dveflem  12782  efhalfpi  12807  efipi  12809  sin2pi  12811  ef2pi  12813  sincosq3sgn  12836  sincosq4sgn  12837  sinq34lt0t  12839  sincos4thpi  12848  tan4thpi  12849  sincos6thpi  12850  sincos3rdpi  12851  pigt3  12852  ex-exp  12866  ex-fac  12867  ex-bc  12868
  Copyright terms: Public domain W3C validator