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  6412  dfplq0qs  6413  genpdf  6491  1prl  6536  1pru  6537  ltexprlemell  6572  ltexprlemelu  6573  recexprlemell  6594  recexprlemelu  6595  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemupu  6621  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdrl  6629  cauappcvgprlem2  6632  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemupu  6643  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem2  6651  addsrpr  6673  mulsrpr  6674  addcnsr  6731  mulcnsr  6732  mulresr  6735  pitonnlem1  6741  axi2m1  6759  axcnre  6765  mulcomli  6832  mnfnre  6865  addcomli  6955  add42i  6974  neg0  7053  negdii  7091  negsubdi2i  7093  crap0  7691  2t2e4  7847  3t2e6  7849  3t3e9  7850  4t2e8  7851  5t2e10  7852  neg1mulneg1e1  7915  8th4div3  7921  halfpm6th  7922  iap0  7925  deceq12i  8150  numltc  8163  decsuc  8166  decsucc  8170  nummac  8175  numma2c  8176  numadd  8177  numaddc  8178  nummul1c  8179  nummul2c  8180  decma  8181  decmac  8182  decma2c  8183  decadd  8184  decaddc  8185  decaddc2  8186  decaddci  8188  decaddci2  8189  decmul1c  8190  decmul2c  8191  6p5e11  8193  7p4e11  8195  8p3e11  8199  4t3lem  8214  6t2e12  8220  7t2e14  8225  8t2e16  8231  9t2e18  8238  divfnzn  8332  xnegpnf  8511  xneg0  8514  iooval2  8554  dfioo2  8613  fzval2  8647  fzsuc2  8711  fztpval  8715  fzo01  8842  fzo12sn  8843  fzo0to42pr  8846  neg1sqe1  9001  sq2  9002  sq3  9003  cu2  9004  i2  9006  i3  9007  binom2i  9013  cji  9130  cnrecnv  9138  sqrt0  9213  absi  9223  bj-dfom  9392