Theorem eqtri 2057

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtri.1	⊢ A = B
eqtri.2	⊢ B = 𝐶

Assertion

Ref	Expression
eqtri	⊢ A = 𝐶

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 ⊢ A = B
2		eqtri.2	. . 3 ⊢ B = 𝐶
3	2	eqeq2i 2047	. 2 ⊢ (A = B ↔ A = 𝐶)
4	1, 3	mpbi 133	1 ⊢ A = 𝐶

Syntax hints:   = wceq 1242

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-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  eqtr2i  2058  eqtr3i  2059  eqtr4i  2060  3eqtri  2061  3eqtrri  2062  3eqtr2i  2063  cbvrab  2549  csb2  2848  cbvrabcsf  2905  difjust  2913  unjust  2915  injust  2917  difeq12i  3054  inrot  3146  symdif1  3196  rabnc  3244  ssdifin0  3298  dfif3  3337  ifbieq2i  3345  ifbieq12i  3347  pwjust  3352  snjust  3372  dfpr2  3383  disjpr2  3425  difprsn1  3494  diftpsn3  3496  dfuni2  3573  intab  3635  intunsn  3644  rint0  3645  iunid  3703  viin  3707  iinrabm  3710  2iunin  3714  riin0  3719  unopab  3827  cbvmpt  3842  unisucg  4117  op1stb  4175  elxpi  4304  csbxpg  4364  relopabi  4406  inxp  4413  coeq12i  4442  dfdm3  4465  dfrn3  4467  dmun  4485  dmopab  4489  dmopab3  4491  rnopab  4524  rnmpt  4525  rncoss  4545  rncoeq  4548  reseq12i  4553  resundi  4568  resindi  4570  resiun1  4573  resopab  4595  mptresid  4603  dfima3  4614  imadisj  4630  ndmima  4645  rnun  4675  rnuni  4678  imaundi  4679  inimass  4683  cnvxp  4685  rnxpm  4695  dminxp  4708  imainrect  4709  cnvcnv3  4713  dmpropg  4736  op1sta  4745  op2ndb  4747  op2nda  4748  resdmres  4755  mptpreima  4757  coundi  4765  coundir  4766  cocnvcnv1  4774  cores2  4776  dfdm2  4795  iotajust  4809  dfiota2  4811  funi  4875  funtp  4895  fntpg  4898  funcnvuni  4911  funcnvres  4915  imadiflem  4921  imadif  4922  imainlem  4923  imain  4924  fnresdisj  4952  mptfng  4967  resdif  5091  fv2  5116  dffv4g  5118  fveq12i  5126  nfvres  5149  0fv  5151  dfimafn2  5166  fnimapr  5176  fvmptss2  5190  fvmptg  5191  fvmpts  5193  fvmpt2  5197  mptfvex  5199  fvopab6  5207  f1ompt  5263  dfmpt  5283  ressnop0  5287  fprg  5289  fvsnun1  5303  fsnunfv  5306  fvpr2g  5311  imauni  5343  fliftfuns  5381  cbvriota  5421  oveq123i  5469  resoprab  5539  mpt2fun  5545  rnmpt2  5553  reldmmpt2  5554  ov  5562  ovigg  5563  ovmpt4g  5565  ovg  5581  caov31  5632  elmpt2cl  5640  f1ocnvd  5644  oprabrexex2  5699  op1st  5715  op2nd  5716  f1stres  5728  f2ndres  5729  unielxp  5742  dfoprab3s  5758  dfoprab4  5760  mpt2mpts  5766  mpt2fvex  5771  oprab2co  5781  df1st2  5782  df2nd2  5783  brtpos0  5808  tposoprab  5836  smores3  5849  tfrlemi14d  5888  rdgisuc1  5911  rdg0  5914  frec0g  5922  frecsuc  5930  df1o2  5952  df2o2  5954  oasuc  5983  omv2  5984  omsuc  5990  ecidsn  6089  qliftfuns  6126  oviec  6148  xpcomco  6236  xpassen  6240  addpiord  6300  mulpiord  6301  dmaddpi  6309  dmmulpi  6310  recmulnqg  6375  1lt2nq  6389  halfnqq  6393  dfmq0qs  6411  dfplq0qs  6412  genpdf  6490  1pr  6534  1prl  6535  1pru  6536  ltexprlemell  6570  ltexprlemelu  6571  recexprlemell  6592  recexprlemelu  6593  addsrpr  6633  mulsrpr  6634  addcnsr  6691  mulcnsr  6692  mulresr  6695  pitonnlem1  6701  axi2m1  6719  axcnre  6725  mulcomli  6792  mnfnre  6825  addcomli  6915  add42i  6934  neg0  7013  negdii  7051  negsubdi2i  7053  crap0  7651  2t2e4  7807  3t2e6  7809  3t3e9  7810  4t2e8  7811  5t2e10  7812  neg1mulneg1e1  7875  8th4div3  7881  halfpm6th  7882  iap0  7885  deceq12i  8110  numltc  8123  decsuc  8126  decsucc  8130  nummac  8135  numma2c  8136  numadd  8137  numaddc  8138  nummul1c  8139  nummul2c  8140  decma  8141  decmac  8142  decma2c  8143  decadd  8144  decaddc  8145  decaddc2  8146  decaddci  8148  decaddci2  8149  decmul1c  8150  decmul2c  8151  6p5e11  8153  7p4e11  8155  8p3e11  8159  4t3lem  8174  6t2e12  8180  7t2e14  8185  8t2e16  8191  9t2e18  8198  divfnzn  8292  xnegpnf  8471  xneg0  8474  iooval2  8514  dfioo2  8573  fzval2  8607  fzsuc2  8671  fztpval  8675  fzo01  8802  fzo12sn  8803  fzo0to42pr  8806  neg1sqe1  8961  sq2  8962  sq3  8963  cu2  8964  i2  8966  i3  8967  binom2i  8973  cji  9090  cnrecnv  9098  bj-dfom  9321