Theorem eqtri 2158

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 2148	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐴 = 𝐶)
4	1, 3	mpbi 144	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  eqtr2i  2159  eqtr3i  2160  eqtr4i  2161  3eqtri  2162  3eqtrri  2163  3eqtr2i  2164  cbvrab  2679  csb2  3000  cbvrabcsf  3060  difjust  3067  unjust  3069  injust  3071  dfdif3  3181  difeq12i  3187  inrot  3286  symdif1  3336  rabnc  3390  0in  3393  ssdifin0  3439  dfif3  3482  ifbieq2i  3490  ifbieq12i  3492  pwjust  3506  snjust  3527  dfpr2  3541  disjpr2  3582  difprsn1  3654  diftpsn3  3656  difpr  3657  dfuni2  3733  intab  3795  intunsn  3804  rint0  3805  iunid  3863  viin  3867  iinrabm  3870  2iunin  3874  riin0  3879  iunxprg  3888  unopab  4002  cbvmptf  4017  cbvmpt  4018  unisucg  4331  op1stb  4394  orddif  4457  elxpi  4550  csbxpg  4615  relopabi  4660  inxp  4668  coeq12i  4697  dfdm3  4721  dfrn3  4723  dmun  4741  dmopab  4745  dmopab3  4747  dmxpid  4755  dmxpin  4756  rnopab  4781  rnmpt  4782  rncoss  4804  rncoeq  4807  reseq12i  4812  resundi  4827  resindi  4829  resiun1  4833  resdmdfsn  4857  resopab  4858  mptresid  4868  dfima3  4879  imadisj  4896  ndmima  4911  mptcnv  4936  rnun  4942  rnuni  4945  imaundi  4946  inimass  4950  cnvxp  4952  rnxpm  4963  dminxp  4978  imainrect  4979  cnvcnv3  4983  dmpropg  5006  op1sta  5015  op2ndb  5017  op2nda  5018  resdmres  5025  mptpreima  5027  coundi  5035  coundir  5036  cocnvcnv1  5044  cores2  5046  dfdm2  5068  iotajust  5082  dfiota2  5084  funi  5150  funtp  5171  fntpg  5174  funcnvuni  5187  funcnvres  5191  imadiflem  5197  imadif  5198  imainlem  5199  imain  5200  fnresdisj  5228  mptfng  5243  resdif  5382  fv2  5409  dffv4g  5411  fveq12i  5420  nfvres  5447  0fv  5449  dfimafn2  5464  fnimapr  5474  fvmptss2  5489  fvmptg  5490  fvmpts  5492  fvmpt2  5497  mptfvex  5499  elfvmptrab  5509  fvopab6  5510  f1ompt  5564  dfmpt  5590  ressnop0  5594  fprg  5596  fvsnun1  5610  fsnunfv  5614  fvpr2g  5620  imauni  5655  fliftfuns  5692  cbvriota  5733  oveq123i  5781  fconstmpo  5859  resoprab  5860  mpofun  5866  rnmpo  5874  reldmmpo  5875  ov  5883  ovigg  5884  ovmpt4g  5886  ovg  5902  caov31  5953  elmpocl  5961  f1ocnvd  5965  oprabrexex2  6021  op1st  6037  op2nd  6038  f1stres  6050  f2ndres  6051  unielxp  6065  dfoprab3s  6081  dfoprab4  6083  mpompts  6089  mpofvex  6094  oprab2co  6108  df1st2  6109  df2nd2  6110  f1od2  6125  brtpos0  6142  tposoprab  6170  smores3  6183  tfrlemi14d  6223  tfr1onlemaccex  6238  tfrcllemaccex  6251  rdgisuc1  6274  rdg0  6277  frec0g  6287  df1o2  6319  df2o2  6321  oasuc  6353  omv2  6354  omsuc  6361  ecidsn  6469  qliftfuns  6506  oviec  6528  mapsncnv  6582  dfixp  6587  xpcomco  6713  xpassen  6717  ssenen  6738  undifdc  6805  unfiin  6807  fidcenumlemrks  6834  fidcenumlemr  6836  sbthlemi5  6842  sbthlemi8  6845  fi0  6856  inf00  6911  djuf1olemr  6932  djuinr  6941  djuin  6942  djuun  6945  casefun  6963  casedm  6964  caseinj  6967  caseinl  6969  caseinr  6970  endjusym  6974  eninl  6975  eninr  6976  djudm  6983  djuinj  6984  fodjuomni  7014  fodjumkv  7027  pm54.43  7039  exmidfodomrlemim  7050  xp2dju  7064  djucomen  7065  djuassen  7066  xpdjuen  7067  addpiord  7117  mulpiord  7118  dmaddpi  7126  dmmulpi  7127  recmulnqg  7192  1lt2nq  7207  halfnqq  7211  dfmq0qs  7230  dfplq0qs  7231  genpdf  7309  1prl  7356  1pru  7357  ltexprlemell  7399  ltexprlemelu  7400  recexprlemell  7423  recexprlemelu  7424  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemopu  7449  cauappcvgprlemupu  7450  cauappcvgprlemdisj  7452  cauappcvgprlemloc  7453  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlemladdrl  7458  cauappcvgprlem2  7461  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemopu  7472  caucvgprlemupu  7473  caucvgprlemdisj  7475  caucvgprlemloc  7476  caucvgprlemcl  7477  caucvgprlemladdfu  7478  caucvgprlemladdrl  7479  caucvgprlem2  7481  caucvgprprlemell  7486  caucvgprprlemelu  7487  caucvgprprlemml  7495  caucvgprprlemmu  7496  caucvgprprlemclphr  7506  caucvgprprlemexbt  7507  caucvgprprlem2  7511  addsrpr  7546  mulsrpr  7547  caucvgsrlemoffres  7601  caucvgsr  7603  suplocsrlempr  7608  addcnsr  7635  mulcnsr  7636  mulresr  7639  addvalex  7645  pitonnlem1  7646  axi2m1  7676  axcnre  7682  mulcomli  7766  mnfnre  7801  addcomli  7900  add42i  7921  mvrraddi  7972  neg0  8001  negdii  8039  negsubdi2i  8041  crap0  8709  2t2e4  8867  3t2e6  8869  3t3e9  8870  4t2e8  8871  neg1mulneg1e1  8925  8th4div3  8932  halfpm6th  8933  iap0  8936  dfdec10  9178  deceq12i  9183  numltc  9200  decsuc  9205  decsucc  9215  nummac  9219  numma2c  9220  numadd  9221  numaddc  9222  nummul1c  9223  nummul2c  9224  decma  9225  decmac  9226  decma2c  9227  decadd  9228  decaddc  9229  decrmanc  9231  decrmac  9232  decaddci  9235  decsubi  9237  decmul1  9238  decmul1c  9239  decmul2c  9240  11multnc  9242  4t3lem  9271  6t2e12  9278  7t2e14  9283  8t2e16  9289  9t2e18  9296  9t11e99  9304  halfthird  9317  5recm6rec  9318  divfnzn  9406  xnegpnf  9604  xneg0  9607  xaddmnf1  9624  xaddmnf2  9625  mnfaddpnf  9627  iooval2  9691  dfioo2  9750  fzval2  9786  fzsuc2  9852  fztpval  9856  fzo01  9986  fzo12sn  9987  fzo0to42pr  9990  fldiv4p1lem1div2  10071  intqfrac2  10085  intfracq  10086  1tonninf  10206  neg1sqe1  10380  sq2  10381  sq3  10382  cu2  10384  i2  10386  i3  10387  binom2i  10394  sq10  10452  3dec  10454  facp1  10469  fac2  10470  fac4  10472  4bc2eq6  10513  hashp1i  10549  pr0hash2ex  10554  hashfzo  10561  hashxp  10565  zfz1isolem1  10576  cji  10667  cnrecnv  10675  sqrt0  10769  resqrexlemover  10775  resqrexlemcalc3  10781  absi  10824  absimle  10849  sumeq12i  11127  summodclem2a  11143  summodc  11145  sum0  11150  fsumsplitf  11170  fsum2dlemstep  11196  fsumabs  11227  fsumiun  11239  0.999...  11283  mertenslem2  11298  prodeq12i  11325  ege2le3  11366  eft0val  11388  cos0  11426  cos1bnd  11455  cos2bnd  11456  3dvdsdec  11551  3dvds2dec  11552  odd2np1  11559  opoe  11581  nn0o  11593  gcd0val  11638  6gcd4e2  11672  3lcm2e6woprm  11756  3lcm2e6  11827  nn0gcdsq  11867  phiprmpw  11887  phimullem  11890  unennn  11899  ennnfonelemj0  11903  ennnfonelem0  11907  ennnfonelem1  11909  ennnfonelemhf1o  11915  ennnfonelemrn  11921  ennnfonelemdm  11922  strnfvnd  11968  slotslfn  11974  setsfun  11983  setsfun0  11984  setscom  11988  setsslid  11998  2strstr1g  12051  cnco  12379  txuni2  12414  txbas  12416  uptx  12432  txcn  12433  cnmptid  12439  cnmpt2t  12451  xmetxp  12665  cnmetdval  12687  remetdval  12697  resubmet  12706  rerestcntop  12708  divcnap  12713  cnrehmeocntop  12751  dvexp  12833  sinhalfpilem  12861  cosneghalfpi  12868  efhalfpi  12869  cospi  12870  efipi  12871  eulerid  12872  sin2pi  12873  cos2pi  12874  ef2pi  12875  sincosq4sgn  12899  cosq14gt0  12902  tangtx  12908  sincos4thpi  12910  sincos6thpi  12912  sinkpi  12917  cosq34lt1  12920  ex-fl  12926  ex-exp  12928  ex-fac  12929  ex-bc  12930  ex-dvds  12931  ex-gcd  12932  bj-dfom  13120  pwle2  13182  exmid1stab  13184  nninfsellemqall  13200  isomninnlem  13214  taupi  13228