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

Theorem oveq12d 5473
Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Hypotheses
Ref Expression
oveq1d.1 (φA = B)
oveq12d.2 (φ𝐶 = 𝐷)
Assertion
Ref Expression
oveq12d (φ → (A𝐹𝐶) = (B𝐹𝐷))

Proof of Theorem oveq12d
StepHypRef Expression
1 oveq1d.1 . 2 (φA = B)
2 oveq12d.2 . 2 (φ𝐶 = 𝐷)
3 oveq12 5464 . 2 ((A = B 𝐶 = 𝐷) → (A𝐹𝐶) = (B𝐹𝐷))
41, 2, 3syl2anc 391 1 (φ → (A𝐹𝐶) = (B𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242  (class class class)co 5455
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458
This theorem is referenced by:  oveq123d  5476  ovmpt2dxf  5568  ovmpt2df  5574  caovdig  5617  caovdir2d  5619  caovdirg  5620  caovdilemd  5634  caovlem2d  5635  offval  5661  fnofval  5663  offval2  5668  ofco  5671  caofinvl  5675  offres  5704  nnmsucr  6006  nndir  6008  ecovdi  6153  ecovidi  6154  dfplpq2  6338  dfmpq2  6339  addcmpblnq  6351  mulpipqqs  6357  addassnqg  6366  distrnqg  6371  ltaddnq  6390  halfnqq  6393  enq0tr  6416  addcmpblnq0  6425  addnq0mo  6429  addnnnq0  6431  nqnq0a  6436  distrnq0  6441  addassnq0  6444  distnq0r  6445  nq02m  6447  ltexpri  6585  mulcmpblnrlemg  6628  mulsrmo  6632  mulsrpr  6634  mulcomsrg  6645  distrsrg  6647  recexgt0sr  6661  mulgt0sr  6664  mulextsr1lem  6666  addcnsr  6691  mulcnsr  6692  axaddcl  6710  axmulcl  6712  axmulcom  6715  axmulass  6717  axdistr  6718  adddir  6776  muladd11  6903  1p1times  6904  pnpcan2  7007  muladd  7137  subdir  7139  mulsub  7154  mulreim  7348  apadd1  7352  mulext1  7356  recextlem1  7374  muleqadd  7391  divdirap  7416  divadddivap  7445  conjmulap  7447  divcanap5rd  7534  cnref1o  8317  icoshftf1o  8589  lincmb01cmp  8601  iccf1o  8602  fz01en  8647  fzrev3  8679  fzrevral2  8698  fzrevral3  8699  fzshftral  8700  fzoaddel2  8779  fzosubel  8780  fzosubel2  8781  fzocatel  8785  frecuzrdgsuc  8842  frecfzen2  8845  iseqovex  8859  mulexp  8908  mulexpzap  8909  expaddzap  8913  expubnd  8925  subsq  8971  binom2  8975  binom21  8976  binom2sub  8977  binom3  8979  crre  9045  replim  9047  remullem  9059  remul2  9061  immul2  9068  cjcj  9071  cjadd  9072  ipcnval  9074  cjmulval  9076  cjneg  9078  imval2  9082  cjreim  9091
  Copyright terms: Public domain W3C validator