Theorem eqtr 1495

Description: An equality transitivity inference.

Hypotheses

Ref	Expression
eqtr.1	|- A = B
eqtr.2	|- B = C

Assertion

Ref	Expression
eqtr	|- A = C

Proof of Theorem eqtr

Step	Hyp	Ref	Expression
1		eqtr.1	. 2 |- A = B
2		eqtr.2	. . 3 |- B = C
3	2	eqeq2i 1485	. 2 |- (A = B <-> A = C)
4	1, 3	mpbi 189	1 |- A = C

Syntax hints:   = wceq 956

This theorem is referenced by:  eqtr2 1496  eqtr3 1497  eqtr4 1498  3eqtr 1499  3eqtr2 1501  3eqtr3 1503  3eqtr4 1505  rabab 1822  difeq12i 2157  dfun3 2246  dfin3 2247  invdif 2249  difundi 2257  difindi 2259  symdif1 2265  undif1 2340  dfif2 2363  dfpr2 2422  dfuni2 2505  intab 2560  intunsn 2565  unopab 2679  op1stb 2913  dfepfr 2932  orddif 3075  onuninsuc 3108  fconstopab 3210  onnev 3242  dfdm3 3302  dfrn3 3304  dmopab 3320  dmopab3 3322  dmxpin 3334  rnopab 3353  rncoss 3364  rncoeq 3367  resundi 3378  resopab 3395  dfima3 3406  imadisj 3422  ndmima 3434  op1sta 3448  op2ndb 3451  op2nda 3452  rnun 3457  imaun 3460  rnxp 3472  dminxp 3483  rescnvcnv 3493  resdmres 3497  cocnvcnv1 3505  cores2 3507  funi 3545  funcnvuni 3564  funcnvres 3568  fnresdisj 3597  fv2 3720  dfimafn2 3762  fvopab4gf 3781  fvsnun1 3795  abrexexlem2 3859  tfrlem3 3913  tfrlem9 3919  tfrlem10 3920  tz7.44-2 3929  dfrdg2 3933  rdglem1 3937  rdgsucopabn 3947  abianfplem 3961  opreq12i 3973  resoprab 4009  oprabval 4023  oprabvalig 4024  oprabval2gf 4026  oprabval5 4029  caopr31 4062  caopr42 4066  caoprdilem 4068  caoprmo 4070  mptg 4075  mpt2g 4076  op1st 4085  op2nd 4086  f1stres 4093  f2ndres 4094  curry1 4098  unielxp 4107  dfopab2 4113  dfoprab3 4114  dfoprab5 4115  df1o2 4140  ecidsn 4287  oprec 4318  fnmap 4329  mapvalg 4330  pmvalg 4331  map0 4344  xpassen 4441  sbthlem5 4451  sbthlem8 4454  fodomr 4483  mapunen 4502  ssenen 4504  limensuci 4506  phplem1 4508  abfii4OLD 4564  abfii5OLD 4565  pm54.43 4572  supex 4577  inf3lema 4609  inf3lemb 4610  trcl 4645  zfregs 4647  r10 4651  rankval 4668  rankuni 4698  ranksuc 4700  rankxpu 4711  rankxplim3 4714  rankxpsuc 4715  kardex 4725  hta 4728  aceq3 4733  ac6lem 4754  kmlem11 4775  kmlem12 4776  zorn2lem1 4788  brdom7disj 4804  brdom6disj 4805  aleph0 4863  alephfplem1 4896  cf0 4910  cdavalt 4919  cdaassen 4930  addpiord 5012  mulpiord 5013  dmaddpi 5018  dmmulpi 5019  addcmpblnq 5052  addcompq 5062  dmrecpq 5074  ltapq 5076  ltmpq 5077  1lt2pq 5078  ltaddpq 5079  mulcomsr 5198  distrsr 5200  ltasr 5209  recexsrlem 5212  sqgt0sr 5215  map2psrpr 5220  supsrlem4 5228  supsrlem5 5229  addcnsr 5253  mulcnsr 5254  mulresr 5257  axmulcom 5276  axmulass 5278  axdistr 5279  axi2m1 5285  axcnre 5286  mulid2 5333  add42 5343  negsub 5381  neg0 5415  mul02 5432  1p1times 5433  mul2neg 5447  negdi 5448  mnfnre 5497  renfdisj 5539  ssxr 5540  ltsubadd 5594  divcan1 5717  divrec 5737  divcan3 5752  divcan4 5753  divid 5770  recgt0i 5814  2times 6003  2t2e4 6022  3t2e6 6023  3t3e9 6024  4t2e8 6025  5t2e10 6026  8th4div3 6031  halfpm6th 6032  infmsup 6068  nneo 6197  uzwo3lem2 6217  intfrac 6253  intfracOLD 6254  intfracqOLD 6255  om2uz0 6295  uzrdgini 6303  seq1lem1 6309  seq1rval 6311  ser11 6335  shftidt 6355  dfioo2 6403  icoshftf1oi 6409  uzinfm 6462  nninfm 6463  nn0infm 6464  seq1seq0t 6544  seq00 6550  ser00 6566  sqreci 6619  sumsqne0 6634  sq2 6638  sq3 6639  cu2 6640  binom2 6644  binom2aOLD 6645  discrlem1 6656  nn0opthlem1 6664  sqrlem10 6682  sqrlem11 6683  sqrlem16 6688  sqrth 6699  sqr2irrlem1 6724  i2 6732  i3 6733  crne0 6739  imret 6773  cjcj 6778  recj 6782  imcj 6783  readd 6784  imadd 6785  remul 6786  immul 6787  cjadd 6788  reneg 6794  imneg 6796  cjneg 6797  cji 6827  absval2 6841  abs00 6842  absmul 6847  absid 6861  abstri 6891  fac0 6934  fac1 6935  facp1t 6936  fac2 6937  faclbnd4lem1 6948  faclbnd4lem4 6951  bcpasc2 6967  sumeq12i 6989  serzfsum 7004  csbfsumlem 7026  dfisum 7191  isumnn0nna 7208  isum0split 7217  fnsmntlem 7225  geoser 7234  geolim1i 7238  0.999... 7246  fsum0diag 7258  fsum0diag2 7259  ivthlem6 7286  ivthlem7 7287  dsupivthlem 7291  ef0lem 7310  efseq0ex 7311  efcvgfsum 7315  erelem2 7320  erelem6 7324  ele3lem 7326  ege2le3lem2 7329  efaddlem5 7342  efaddlem8 7345  efaddlem20 7357  efaddlem22 7359  ef1tllem 7381  eirrlem1 7389  eirrlem2 7390  efsep 7396  ef4p 7399  reeff1 7410  efm1lim 7411  sin0 7444  cos0 7446  sinadd 7451  cosadd 7452  cos1bnd 7474  cos2bnd 7475  acdc3lem 7486  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  ruclem2 7511  ruclem3 7512  ruclem14 7523  ruclem15 7524  infxpidmlem6 7557  infxpidmlem11 7562  infmap2lem1 7579  subbas2OLD 7645  subtop 7646  indistop 7648  fctopOLD 7650  cctop 7652  uniretop 7657  cnco 7768  dfms2 7799  metssba 7809  cnmetdval 7902  cnmetba 7903  cncfmet 7905  cncfmet1 7906  remetdval 7908  oprcn 7977  bcthlem9 8007  issubg 8116  grpsn 8124  ringsn 8163  vcm 8190  vcnegneg 8193  vafval 8222  smfval 8224  nmfval 8226  nvnncan 8283  nvm1 8292  nvpi 8294  nvmtri 8299  cnnvg 8308  cnnvs 8311  abscn 8343  ipval2lem1 8351  ipval2 8357  ipid 8363  ip0r 8370  nmblolbii 8459  blocnilem 8464  ip2i 8487  ipdirilem 8488  ipasslem10 8499  siilem1 8511  siii 8513  minvecex 8578  spwval2 8653  pilem1 8671  pilem3 8673  sinhalfpilem 8679  cospi 8682  eulerid 8683  sin2pi 8684  cos2pi 8685  sinperlem1 8686  sincosq4sgn 8707  sincos4thpi 8710  sincos6thpi 8711  cosh111lem1 8714  effoi 8745  pilog 8768  grothprim 8783  avril1 8784  hvsubass 8922  hvnegdi 8929  hvsubeq0 8930  hvsubcan2 8931  normlem0 8975  normlem1 8976  normlem9 8984  normsq 8999  norm-ii 9004  norm-iii 9006  normsub 9008  normpar 9021  normpar2 9023  polid2 9024  bcsALT 9046  hhssva 9129  hhsssm 9130  hhssnv 9134  hhshsslem1 9137  hhsssh2 9140  projlem3 9188  projlem4 9189  projlem7 9192  projlem18 9203  pjthlem1 9219  ococ 9247  dfchsup2 9298  dfchj2 9324  dfchj3 9325  chdmm2 9401  chdmm3 9402  chdmm4 9403  chdmj2 9405  chdmj3 9406  chdmj4 9407  chjo 9411  h1de2 9476  spanunsn 9502  pjoml3 9529  pjoml4 9530  cmbr2 9539  cmbr3 9543  qlax5 9572  qlaxr2 9574  osumcor2 9590  pjadj 9618  pjadd 9620  pjmul 9622  pjsub 9623  pjssm 9626  pjdifnorm 9628  pjcj 9629  pjpyth 9667  dfiop2 9679  hoid1 9715  hoid1r 9716  honegnegt 9732  hosd1 9748  hosubeq0 9752  ho01 9754  dfadj2 9812  cnvadj 9816  adj1o 9818  dmadjss 9819  hhlno 9826  hh0o 9829  lnop0t 9890  nmop0h 9916  lnopunilem1 9935  lnophmlem2 9942  nmbdoplb 9949  lnfn0 9971  cnlnadjlem5 10004  adjbdlnt 10016  nmoptri2 10032  kbass2t 10050  kbass5t 10053  mdsl1 10248  cvmd 10251  mdsldmd1 10258  mdslmd3 10259  mdexch 10262  shatomistic 10288  cvexch 10296  atord 10311  sumdmdlem2 10346  ghomgrpilem2 10386  ghomgrp 10390  symgval 10403  symggrpi 10406  symgidi 10407  cayleylem3 10411  oprabvaligg 10440  fopab2ga 10465  fopab2a 10466  dmhmph 10532  rnhmph 10533  top2usne 10549  subsp 10554  domval 10655  codval 10656  idval 10657  cmpval 10658  1ded 10671  1cat 10692  dmo 10709  cmpmorp 10712  ishomb 10716  mrdmcd 10722  homib 10724  cmphmia 10726  cmphmib 10727  iri 10728  idmon 10745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain