Theorem eqtr 1487

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 1477	. 2 |- (A = B <-> A = C)
4	1, 3	mpbi 189	1 |- A = C

Syntax hints:   = wceq 953

This theorem is referenced by:  eqtr2 1488  eqtr3 1489  eqtr4 1490  3eqtr 1491  3eqtr2 1493  3eqtr3 1495  3eqtr4 1497  rabab 1813  difeq12i 2147  dfun3 2236  dfin3 2237  invdif 2239  difundi 2247  difindi 2249  symdif1 2255  undif1 2330  dfif2 2353  dfpr2 2412  dfuni2 2495  intab 2550  intunsn 2555  unopab 2669  op1stb 2903  dfepfr 2922  orddif 3065  onuninsuc 3098  fconstopab 3200  onnev 3232  dfdm3 3291  dfrn3 3293  dmopab 3309  dmopab3 3311  dmxpin 3323  rnopab 3339  rncoss 3348  rncoeq 3351  resundi 3362  resopab 3379  dfima3 3390  imadisj 3406  ndmima 3418  op1sta 3434  op2ndb 3437  op2nda 3438  rnun 3443  imaun 3446  rnxp 3458  dminxp 3469  rescnvcnv 3479  resdmres 3483  cocnvcnv1 3491  cores2 3493  unidmrnOLD 3502  funi 3531  funcnvuni 3550  funcnvres 3554  fnresdisj 3583  fv2 3705  dfimafn2 3747  fvopab4gf 3766  fvsnun1 3780  abrexexlem2 3844  tfrlem3 3898  tfrlem9 3904  tfrlem10 3905  tz7.44-2 3914  dfrdg2 3918  rdglem1 3922  rdgsucopabn 3932  abianfplem 3946  opreq12i 3958  resoprab 3994  oprabval 4008  oprabvalig 4009  oprabval2gf 4011  oprabval5 4014  caopr31 4048  caopr42 4052  caoprdilem 4054  caoprmo 4056  op1st 4069  op2nd 4070  f1stres 4077  f2ndres 4078  curry1 4082  unielxp 4091  dfopab2 4097  dfoprab3 4098  dfoprab5 4099  df1o2 4124  ecidsn 4271  oprec 4302  fnmap 4313  mapvalg 4314  pmvalg 4315  map0 4328  xpassen 4421  sbthlem5 4431  sbthlem8 4434  fodomr 4463  mapunen 4482  ssenen 4484  limensuci 4486  phplem1 4488  abfii4 4538  abfii5 4539  pm54.43 4546  supex 4551  inf3lema 4581  inf3lemb 4582  trcl 4617  zfregs 4619  r10 4623  rankval 4640  rankuni 4670  ranksuc 4672  rankxpu 4683  rankxplim3 4686  rankxpsuc 4687  kardex 4697  hta 4700  aceq3 4705  ac6lem 4726  kmlem11 4747  kmlem12 4748  zorn2lem1 4760  brdom7disj 4776  brdom6disj 4777  aleph0 4835  alephfplem1 4868  cf0 4882  cdavalt 4891  cdaassen 4902  addpiord 4984  mulpiord 4985  dmaddpi 4990  dmmulpi 4991  addcmpblnq 5024  addcompq 5034  dmrecpq 5046  ltapq 5048  ltmpq 5049  1lt2pq 5050  ltaddpq 5051  mulcomsr 5170  distrsr 5172  ltasr 5181  recexsrlem 5184  sqgt0sr 5187  map2psrpr 5192  supsrlem4 5200  supsrlem5 5201  addcnsr 5225  mulcnsr 5226  mulresr 5229  axmulcom 5248  axmulass 5250  axdistr 5251  axi2m1 5257  axcnre 5258  mulid2 5305  add42 5315  negsub 5353  neg0 5387  mul02 5404  1p1times 5405  mul2neg 5419  negdi 5420  mnfnre 5469  renfdisj 5512  ssxr 5513  ltsubadd 5568  divcan1 5686  divrec 5700  divcan3 5714  divcan4 5715  divid 5726  recgt0i 5770  2times 5950  2t2e4 5969  3t2e6 5970  3t3e9 5971  4t2e8 5972  5t2e10 5973  8th4div3 5978  halfpm6th 5979  infmsup 6015  nneo 6144  uzwo3lem2 6165  om2uz0 6232  uzrdgini 6240  seq1lem1 6246  seq1rval 6248  ser11 6272  shftidt 6292  dfioo2 6336  icoshftf1oi 6342  uzinfm 6394  nninfm 6395  nn0infm 6396  seq1seq0t 6476  seq00 6482  ser00 6498  sqreci 6549  sumsqne0 6565  sq2 6569  sq3 6570  cu2 6571  binom2 6575  binom2aOLD 6576  discrlem1 6586  nn0opthlem1 6594  sqrlem10 6612  sqrlem11 6613  sqrlem16 6618  sqrth 6629  sqr2irrlem1 6654  i2 6662  i3 6663  crne0 6670  cjcj 6713  recj 6717  imcj 6718  readd 6719  imadd 6720  remul 6721  immul 6722  cjadd 6723  reneg 6729  imneg 6731  cjneg 6732  cji 6762  absval2 6776  abs00 6777  absmul 6782  absid 6796  abstri 6829  fac0 6871  fac1 6872  facp1t 6873  fac2 6874  faclbnd4lem1 6885  faclbnd4lem4 6888  bcpasc2 6905  sumeq12i 6927  serzfsum 6942  csbfsumlem 6964  dfisum 7127  isumnn0nna 7143  isum0split 7152  fnsmntlem 7160  geoser 7169  geolim1i 7173  0.999... 7181  fsum0diag 7193  fsum0diag2 7194  ivthlem6 7221  ivthlem7 7222  dsupivthlem 7226  ivthlem6OLD 7230  ivthlem7OLD 7231  ef0lem 7252  efseq0ex 7253  efcvgfsum 7257  erelem2 7262  erelem6 7266  ele3lem 7268  ege2le3lem2 7271  efaddlem5 7284  efaddlem8 7287  efaddlem20 7299  efaddlem22 7301  ef1tllem 7323  eirrlem1 7330  eirrlem2 7331  efsep 7337  ef4p 7340  reeff1 7350  efm1lim 7351  sin0 7386  cos0 7388  sinadd 7393  cosadd 7394  cos1bnd 7416  cos2bnd 7417  acdc3lem 7428  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  ruclem2 7454  ruclem3 7455  ruclem14 7466  ruclem15 7467  infxpidmlem6 7500  infxpidmlem11 7505  infmap2lem1 7521  subbas2 7587  subtop 7588  indistop 7590  fctop 7592  cctop 7594  uniretop 7599  cnco 7707  dfms2 7738  metssba 7748  cnmetdval 7841  cnmetba 7842  cncfmet 7844  cncfmet1 7845  remetdval 7847  oprcn 7911  bcthlem9 7941  issubg 8053  grpsn 8061  ringsn 8100  vcm 8127  vcnegneg 8130  vafval 8160  smfval 8162  nmfval 8164  nvnncan 8223  nvm1 8231  nvpi 8233  nvmtri 8238  cnnvg 8246  cnnvs 8249  abscn 8277  ipval2lem1 8285  ipval2 8291  ipid 8297  ip0r 8304  nmblolbii 8390  blocnilem 8395  ip2i 8418  ipdirilem 8419  ipasslem10 8430  siilem1 8442  siii 8444  minvecex 8509  spwval2 8577  pilem1 8590  pilem3 8592  sinhalfpilem 8598  cospi 8601  eulerid 8602  sin2pi 8603  cos2pi 8604  sinperlem1 8605  sincosq4sgn 8624  sincos4thpi 8627  sincos6thpi 8628  cosh111lem1 8629  effoi 8666  effoiOLD 8667  pilog 8690  dflog2OLD 8701  grothprim 8722  avril1 8723  hvsubass 8843  hvnegdi 8850  hvsubeq0 8851  hvsubcan2 8852  normlem0 8896  normlem1 8897  normlem9 8905  normsq 8920  norm-ii 8925  norm-iii 8927  normsub 8929  normpar 8942  normpar2 8944  polid2 8945  bcsALT 8967  hhssva 9050  hhsssm 9051  hhssnv 9054  hhshsslem1 9057  projlem3 9104  projlem4 9105  projlem7 9108  projlem18 9119  pjthlem1 9134  ococ 9162  dfchsup2 9213  dfchj2 9239  dfchj3 9240  chdmm2 9316  chdmm3 9317  chdmm4 9318  chdmj2 9320  chdmj3 9321  chdmj4 9322  chjo 9326  h1de2 9391  spanunsn 9419  pjoml3 9446  pjoml4 9447  cmbr2 9456  cmbr3 9460  qlax5 9489  qlaxr2 9491  osumcor2 9507  pjadj 9535  pjadd 9537  pjmul 9539  pjsub 9540  pjssm 9543  pjdifnorm 9545  pjcj 9546  pjpyth 9584  dfiop2 9596  hoid1 9632  hoid1r 9633  honegnegt 9649  hosd1 9665  hosubeq0 9669  ho01 9671  dfadj2 9729  cnvadj 9733  adj1o 9735  dmadjss 9736  hhlno 9743  hh0o 9746  lnop0t 9806  nmop0h 9831  lnopunilem1 9850  lnophmlem2 9857  nmbdoplb 9864  lnfn0 9886  cnlnadjlem5 9919  adjbdlnt 9931  nmoptri2 9946  kbass2t 9962  kbass5t 9965  mdsl1 10156  cvmd 10159  mdsldmd1 10166  mdslmd3 10167  mdexch 10170  shatomistic 10196  cvexch 10204  atord 10219  sumdmdlem2 10253  ghomgrpilem2 10291  ghomgrp 10295  symgval 10308  symggrpiOLD 10311  symgidiOLD 10312  symggrpi 10313  symgidi 10314  cayleylem3 10318  oprabvaligg 10341  fopab2ga 10361  fopab2a 10362  dmhmph 10419  rnhmph 10420  subsp 10429  domval 10499  codval 10500  idval 10501  cmpval 10502  1ded 10515  1cat 10536  dmo 10553  cmpmorp 10556  ishomb 10560  mrdmcd 10566  homib 10568  cmphmia 10570  cmphmib 10571  iri 10572  idmon 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain