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

Theorem oveq12d 5558
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  |-  ( ph  ->  A  =  B )
oveq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
oveq12d  |-  ( ph  ->  ( A F C )  =  ( B F D ) )

Proof of Theorem oveq12d
StepHypRef Expression
1 oveq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 oveq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 oveq12 5549 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3syl2anc 397 1  |-  ( ph  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259  (class class class)co 5540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-br 3793  df-iota 4895  df-fv 4938  df-ov 5543
This theorem is referenced by:  oveq123d  5561  ovmpt2dxf  5654  ovmpt2df  5660  caovdig  5703  caovdir2d  5705  caovdirg  5706  caovdilemd  5720  caovlem2d  5721  offval  5747  fnofval  5749  offval2  5754  ofco  5757  caofinvl  5761  offres  5790  nnmsucr  6098  nndir  6100  ecovdi  6248  ecovidi  6249  dfplpq2  6510  dfmpq2  6511  addcmpblnq  6523  mulpipqqs  6529  addassnqg  6538  distrnqg  6543  ltaddnq  6563  halfnqq  6566  enq0tr  6590  addcmpblnq0  6599  addnq0mo  6603  addnnnq0  6605  nqnq0a  6610  distrnq0  6615  addassnq0  6618  distnq0r  6619  nq02m  6621  ltexpri  6769  cauappcvgprlemm  6801  cauappcvgprlemloc  6808  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlem1  6815  cauappcvgprlem2  6816  cauappcvgprlemlim  6817  cauappcvgpr  6818  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemm  6824  caucvgprlemloc  6831  caucvgprlemcl  6832  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem2  6836  caucvgpr  6838  caucvgprprlemelu  6842  caucvgprprlemcbv  6843  caucvgprprlemval  6844  caucvgprprlemmu  6851  caucvgprprlemopu  6855  caucvgprprlemloc  6859  caucvgprprlemclphr  6861  caucvgprprlemexbt  6862  caucvgprprlem2  6866  mulcmpblnrlemg  6883  mulsrmo  6887  mulsrpr  6889  mulcomsrg  6900  distrsrg  6902  recexgt0sr  6916  mulgt0sr  6920  mulextsr1lem  6922  caucvgsrlemgt1  6937  caucvgsr  6944  addcnsr  6968  mulcnsr  6969  recidpirqlemcalc  6991  axaddcl  6998  axmulcl  7000  axmulcom  7003  axmulass  7005  axdistr  7006  axcaucvglemcau  7030  axcaucvglemres  7031  adddir  7076  muladd11  7207  1p1times  7208  muladd11r  7230  pnpcan2  7314  muladd  7453  subdir  7455  mulsub  7470  mulreim  7669  apadd1  7673  mulext1  7677  recextlem1  7706  muleqadd  7723  divdirap  7748  divadddivap  7778  conjmulap  7780  divcanap5rd  7867  xp1d2m1eqxm1d2  8234  div4p1lem1div2  8235  cnref1o  8680  icoshftf1o  8960  lincmb01cmp  8972  iccf1o  8973  fz01en  9019  fzrev3  9051  fzrevral2  9070  fzrevral3  9071  fzshftral  9072  fzoaddel2  9151  fzosubel  9152  fzosubel2  9153  fzocatel  9157  modqsubdir  9343  addmodlteq  9348  frecuzrdgsuc  9365  frecfzen2  9368  iseqovex  9383  iseqcaopr3  9404  iseqid3s  9410  iseqdistr  9414  serile  9418  mulexp  9459  mulexpzap  9460  expaddzap  9464  expubnd  9477  subsq  9525  binom2  9529  binom21  9530  binom2sub  9531  binom3  9534  sqoddm1div8  9569  nn0opthlem1d  9588  nn0opthd  9590  facp1  9598  facubnd  9613  bcval  9617  bcn1  9626  bcm1k  9628  bcp1n  9629  bcp1nk  9630  ibcval5  9631  bcn2  9632  bcpasc  9634  crre  9685  replim  9687  remullem  9699  remul2  9701  immul2  9708  cjcj  9711  cjadd  9712  ipcnval  9714  cjmulval  9716  cjneg  9718  imval2  9722  cjreim  9731  cvg1nlemcau  9811  cvg1nlemres  9812  resqrexlemp1rp  9833  resqrexlemfp1  9836  resqrexlemcalc1  9841  resqrexlemcalc2  9842  resqrex  9853  sqabsadd  9882  sqabssub  9883  absreimsq  9894  recan  9936  amgm2  9945  subcn2  10063  climle  10085  climcvg1nlem  10099  serif0  10102  dvds2ln  10140  odd2np1lem  10183  oddpwdclemdc  10261
  Copyright terms: Public domain W3C validator