Theorem opreq12i 4894

Description: Equality inference for operation value. (The proof was shortened by Andrew Salmon, 22-Oct-2011.)

Hypotheses

Ref	Expression
opreq1i.1	|- A = B
opreq12i.2	|- C = D

Assertion

Ref	Expression
opreq12i	|- (AFC) = (BFD)

Proof of Theorem opreq12i

Step	Hyp	Ref	Expression
1		opreq1i.1	. 2 |- A = B
2		opreq12i.2	. 2 |- C = D
3		opreq12 4891	. 2 |- ((A = B /\ C = D) -> (AFC) = (BFD))
4	1, 2, 3	mp2an 761	1 |- (AFC) = (BFD)

Syntax hints:   = wceq 1298  (class class class)co 4884

This theorem is referenced by:  caoprdistrr 5000  caoprdilem 5001  caoprlem2 5002  addcmpblnq 6204  addcompq 6214  addasspq 6215  distrpq 6219  1lt2pq 6230  mulcomsr 6350  distrsr 6352  m1p1sr 6353  m1m1sr 6354  mulgt0sr 6366  addcnsrec 6415  mulcnsrec 6416  axmulcom 6429  axmulass 6431  axdistr 6432  axi2m1 6438  1p1timesi 6596  mulneg1i 6608  negdii 6611  negdiiOLD 6612  divdiri 6930  3t3e9 7208  halfpm6th 7218  nneoi 7409  icoshftf1oii 7578  ser1add2i 7751  ser1addi 7752  seq1seqz 7784  seq0seqz 7785  seq01 7795  sqdivi 7863  sumsqne0i 7879  binom2i 7890  binom2aiOLD 7891  discrlem1 7906  nnesqi 7912  nn0opthlem1 7914  sqrlem11 7933  sqrlem16 7938  sqrthi 7949  sqrmulii 7954  i4 7984  crmuli 7990  crreczi 7991  cjcji 8028  readdi 8034  imaddi 8035  remuli 8036  immuli 8037  cjaddi 8038  cjmuli 8039  ipcni 8040  cjmulvali 8042  cjnegi 8047  addcji 8048  cji 8077  absmuli 8098  abs1mi 8156  abslem2i 8160  facp1 8188  fac2 8189  fac3 8190  faclbnd4lem1 8200  bcpasc2i 8219  isumnn0nnai 8469  0.999... 8508  dfef2i 8569  efaddlem5 8604  efaddlem6 8605  efaddlem12 8611  eirrlem3 8653  efsepi 8661  eft0vali 8663  ef4pi 8664  efge1pi 8667  efcnlem2 8685  sinaddi 8716  cosaddi 8717  cos2OLD 8730  sin01bndlem3 8735  cos2bnd 8741  ruclem15 8793  bcthlem32 9308  ipval2lem1 9690  ipval2 9696  ip0i 9825  ip1ilem 9826  ip2i 9828  ipdirilem 9829  ipasslem10 9840  ip2dii 9845  pythi 9851  siilem1 9852  eulerid 10032  sin2pi 10033  sinperlem1 10035  sincosq3sgn 10055  sincosq4sgn 10056  sinq34lt0t 10058  sincos4thpi 10060  sincos6thpi 10061  hvsubsub4i 10558  hvsubcan2i 10563  hisubcomi 10603  normlem0 10608  normlem1 10609  normlem2 10610  normlem3 10611  normlem6 10614  normlem8 10616  normlem9 10617  bcseqi 10619  norm-ii.i 10637  norm-iii.i 10639  normpythi 10642  norm3difi 10647  normpari 10654  normpar2i 10656  polid2i 10657  polidi 10658  bcsiALT 10679  projlem3 10821  projlem4 10822  pjthlem5 10856  lediri 11093  h1de2i 11109  cmcmlem 11167  cmbr2i 11172  cm2j 11196  fh3i 11199  fh4i 11200  pjaddii 11255  pjsslem 11259  pjssmii 11261  pjdifnormii 11263  hhlnoi 11463  lnopeq0lem1 11567  lnopunilem1 11572  lnophmlem2 11579  pjsdi2i 11729  pjclem1 11768  golem1 11843  gcdaddmlem 13734  opreq123i 14410  3timesi 14523  topgrpsubcn 14982  1cat 15106  trirni 15833  cnresoprab2 15916  bfplem6 16003  phtpycolem3 16053  phtpycolem4 16054  pcoass 16085  pcorevlem 16086

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014  df-opr 4886

Copyright terms: Public domain