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  1prl  6535  1pru  6536  ltexprlemell  6571  ltexprlemelu  6572  recexprlemell  6593  recexprlemelu  6594  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemopu  6619  cauappcvgprlemupu  6620  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdrl  6628  cauappcvgprlem2  6631  addsrpr  6653  mulsrpr  6654  addcnsr  6711  mulcnsr  6712  mulresr  6715  pitonnlem1  6721  axi2m1  6739  axcnre  6745  mulcomli  6812  mnfnre  6845  addcomli  6935  add42i  6954  neg0  7033  negdii  7071  negsubdi2i  7073  crap0  7671  2t2e4  7827  3t2e6  7829  3t3e9  7830  4t2e8  7831  5t2e10  7832  neg1mulneg1e1  7895  8th4div3  7901  halfpm6th  7902  iap0  7905  deceq12i  8130  numltc  8143  decsuc  8146  decsucc  8150  nummac  8155  numma2c  8156  numadd  8157  numaddc  8158  nummul1c  8159  nummul2c  8160  decma  8161  decmac  8162  decma2c  8163  decadd  8164  decaddc  8165  decaddc2  8166  decaddci  8168  decaddci2  8169  decmul1c  8170  decmul2c  8171  6p5e11  8173  7p4e11  8175  8p3e11  8179  4t3lem  8194  6t2e12  8200  7t2e14  8205  8t2e16  8211  9t2e18  8218  divfnzn  8312  xnegpnf  8491  xneg0  8494  iooval2  8534  dfioo2  8593  fzval2  8627  fzsuc2  8691  fztpval  8695  fzo01  8822  fzo12sn  8823  fzo0to42pr  8826  neg1sqe1  8981  sq2  8982  sq3  8983  cu2  8984  i2  8986  i3  8987  binom2i  8993  cji  9110  cnrecnv  9118  sqrt0  9193  absi  9203  bj-dfom  9367