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

Theorem oveq12i 5793
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 5790 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3mp2an 423 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Colors of variables: wff set class
Syntax hints:   = wceq 1332  (class class class)co 5781
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-iota 5095  df-fv 5138  df-ov 5784
This theorem is referenced by:  oveq123i  5795  1lt2nq  7237  halfnqq  7241  caucvgprprlemnbj  7524  caucvgprprlemaddq  7539  m1p1sr  7591  m1m1sr  7592  axi2m1  7706  negdii  8069  3t3e9  8900  8th4div3  8962  halfpm6th  8963  numma  9248  decmul10add  9273  4t3lem  9301  9t11e99  9334  halfthird  9347  5recm6rec  9348  sqdivapi  10406  sq4e2t8  10420  i4  10425  binom2i  10431  facp1  10507  fac2  10508  fac3  10509  fac4  10510  4bc2eq6  10551  cji  10705  fsumadd  11206  fsumsplitf  11208  fsumsplitsnun  11219  0.999...  11321  ef01bndlem  11497  cos2bnd  11501  3dvds2dec  11597  flodddiv4  11665  nn0gcdsq  11912  cnmpt2res  12503  txmetcnp  12724  dveflem  12893  efhalfpi  12926  efipi  12928  sin2pi  12930  ef2pi  12932  sincosq3sgn  12955  sincosq4sgn  12956  sinq34lt0t  12958  sincos4thpi  12967  tan4thpi  12968  sincos6thpi  12969  sincos3rdpi  12970  pigt3  12971  ex-exp  13108  ex-fac  13109  ex-bc  13110
  Copyright terms: Public domain W3C validator