Theorem eqtri 2060

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

Hypotheses

Ref	Expression
eqtri.1	⊢ 𝐴 = 𝐵
eqtri.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eqtri	⊢ 𝐴 = 𝐶

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	eqeq2i 2050	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐴 = 𝐶)
4	1, 3	mpbi 133	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1243

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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

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

This theorem is referenced by:  eqtr2i  2061  eqtr3i  2062  eqtr4i  2063  3eqtri  2064  3eqtrri  2065  3eqtr2i  2066  cbvrab  2555  csb2  2854  cbvrabcsf  2911  difjust  2919  unjust  2921  injust  2923  difeq12i  3060  inrot  3152  symdif1  3202  rabnc  3250  ssdifin0  3304  dfif3  3343  ifbieq2i  3351  ifbieq12i  3353  pwjust  3360  snjust  3380  dfpr2  3394  disjpr2  3434  difprsn1  3503  diftpsn3  3505  dfuni2  3582  intab  3644  intunsn  3653  rint0  3654  iunid  3712  viin  3716  iinrabm  3719  2iunin  3723  riin0  3728  unopab  3836  cbvmpt  3851  unisucg  4151  op1stb  4209  orddif  4271  elxpi  4361  csbxpg  4421  relopabi  4463  inxp  4470  coeq12i  4499  dfdm3  4522  dfrn3  4524  dmun  4542  dmopab  4546  dmopab3  4548  rnopab  4581  rnmpt  4582  rncoss  4602  rncoeq  4605  reseq12i  4610  resundi  4625  resindi  4627  resiun1  4630  resopab  4652  mptresid  4660  dfima3  4671  imadisj  4687  ndmima  4702  rnun  4732  rnuni  4735  imaundi  4736  inimass  4740  cnvxp  4742  rnxpm  4752  dminxp  4765  imainrect  4766  cnvcnv3  4770  dmpropg  4793  op1sta  4802  op2ndb  4804  op2nda  4805  resdmres  4812  mptpreima  4814  coundi  4822  coundir  4823  cocnvcnv1  4831  cores2  4833  dfdm2  4852  iotajust  4866  dfiota2  4868  funi  4932  funtp  4952  fntpg  4955  funcnvuni  4968  funcnvres  4972  imadiflem  4978  imadif  4979  imainlem  4980  imain  4981  fnresdisj  5009  mptfng  5024  resdif  5148  fv2  5173  dffv4g  5175  fveq12i  5183  nfvres  5206  0fv  5208  dfimafn2  5223  fnimapr  5233  fvmptss2  5247  fvmptg  5248  fvmpts  5250  fvmpt2  5254  mptfvex  5256  fvopab6  5264  f1ompt  5320  dfmpt  5340  ressnop0  5344  fprg  5346  fvsnun1  5360  fsnunfv  5363  fvpr2g  5368  imauni  5400  fliftfuns  5438  cbvriota  5478  oveq123i  5526  resoprab  5597  mpt2fun  5603  rnmpt2  5611  reldmmpt2  5612  ov  5620  ovigg  5621  ovmpt4g  5623  ovg  5639  caov31  5690  elmpt2cl  5698  f1ocnvd  5702  oprabrexex2  5757  op1st  5773  op2nd  5774  f1stres  5786  f2ndres  5787  unielxp  5800  dfoprab3s  5816  dfoprab4  5818  mpt2mpts  5824  mpt2fvex  5829  oprab2co  5839  df1st2  5840  df2nd2  5841  brtpos0  5867  tposoprab  5895  smores3  5908  tfrlemi14d  5947  rdgisuc1  5971  rdg0  5974  frec0g  5983  frecsuc  5991  df1o2  6013  df2o2  6015  oasuc  6044  omv2  6045  omsuc  6051  ecidsn  6153  qliftfuns  6190  oviec  6212  xpcomco  6300  xpassen  6304  addpiord  6414  mulpiord  6415  dmaddpi  6423  dmmulpi  6424  recmulnqg  6489  1lt2nq  6504  halfnqq  6508  dfmq0qs  6527  dfplq0qs  6528  genpdf  6606  1prl  6653  1pru  6654  ltexprlemell  6696  ltexprlemelu  6697  recexprlemell  6720  recexprlemelu  6721  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemupu  6747  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdrl  6755  cauappcvgprlem2  6758  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemupu  6770  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem2  6778  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgprprlem2  6808  addsrpr  6830  mulsrpr  6831  caucvgsrlemoffres  6884  caucvgsr  6886  addcnsr  6910  mulcnsr  6911  mulresr  6914  addvalex  6920  pitonnlem1  6921  axi2m1  6949  axcnre  6955  mulcomli  7034  mnfnre  7068  addcomli  7158  add42i  7177  mvrraddi  7228  neg0  7257  negdii  7295  negsubdi2i  7297  crap0  7910  2t2e4  8069  3t2e6  8071  3t3e9  8072  4t2e8  8073  5t2e10  8074  neg1mulneg1e1  8137  8th4div3  8144  halfpm6th  8145  iap0  8148  deceq12i  8374  numltc  8387  decsuc  8390  decsucc  8394  nummac  8399  numma2c  8400  numadd  8401  numaddc  8402  nummul1c  8403  nummul2c  8404  decma  8405  decmac  8406  decma2c  8407  decadd  8408  decaddc  8409  decaddc2  8410  decaddci  8412  decaddci2  8413  decmul1c  8414  decmul2c  8415  6p5e11  8417  7p4e11  8419  8p3e11  8423  4t3lem  8438  6t2e12  8444  7t2e14  8449  8t2e16  8455  9t2e18  8462  divfnzn  8556  xnegpnf  8741  xneg0  8744  iooval2  8784  dfioo2  8843  fzval2  8877  fzsuc2  8941  fztpval  8945  fzo01  9072  fzo12sn  9073  fzo0to42pr  9076  fldiv4p1lem1div2  9147  intqfrac2  9161  intfracq  9162  neg1sqe1  9348  sq2  9349  sq3  9350  cu2  9351  i2  9353  i3  9354  binom2i  9360  cji  9502  cnrecnv  9510  sqrt0  9602  resqrexlemover  9608  resqrexlemcalc3  9614  absi  9657  absimle  9680  ex-fl  9895  bj-dfom  10057