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  6417  addcmpblnq0  6426  addnq0mo  6430  addnnnq0  6432  nqnq0a  6437  distrnq0  6442  addassnq0  6445  distnq0r  6446  nq02m  6448  ltexpri  6587  cauappcvgprlemm  6617  cauappcvgprlemloc  6624  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlem2  6632  cauappcvgprlemlim  6633  cauappcvgpr  6634  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem2  6651  caucvgpr  6653  mulcmpblnrlemg  6668  mulsrmo  6672  mulsrpr  6674  mulcomsrg  6685  distrsrg  6687  recexgt0sr  6701  mulgt0sr  6704  mulextsr1lem  6706  addcnsr  6731  mulcnsr  6732  axaddcl  6750  axmulcl  6752  axmulcom  6755  axmulass  6757  axdistr  6758  adddir  6816  muladd11  6943  1p1times  6944  pnpcan2  7047  muladd  7177  subdir  7179  mulsub  7194  mulreim  7388  apadd1  7392  mulext1  7396  recextlem1  7414  muleqadd  7431  divdirap  7456  divadddivap  7485  conjmulap  7487  divcanap5rd  7574  cnref1o  8357  icoshftf1o  8629  lincmb01cmp  8641  iccf1o  8642  fz01en  8687  fzrev3  8719  fzrevral2  8738  fzrevral3  8739  fzshftral  8740  fzoaddel2  8819  fzosubel  8820  fzosubel2  8821  fzocatel  8825  frecuzrdgsuc  8882  frecfzen2  8885  iseqovex  8899  mulexp  8948  mulexpzap  8949  expaddzap  8953  expubnd  8965  subsq  9011  binom2  9015  binom21  9016  binom2sub  9017  binom3  9019  crre  9085  replim  9087  remullem  9099  remul2  9101  immul2  9108  cjcj  9111  cjadd  9112  ipcnval  9114  cjmulval  9116  cjneg  9118  imval2  9122  cjreim  9131
  Copyright terms: Public domain W3C validator