Theorem eqtri 2135

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

Syntax hints:   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

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

This theorem is referenced by:  eqtr2i  2136  eqtr3i  2137  eqtr4i  2138  3eqtri  2139  3eqtrri  2140  3eqtr2i  2141  cbvrab  2655  csb2  2973  cbvrabcsf  3031  difjust  3038  unjust  3040  injust  3042  dfdif3  3152  difeq12i  3158  inrot  3257  symdif1  3307  rabnc  3361  0in  3364  ssdifin0  3410  dfif3  3453  ifbieq2i  3461  ifbieq12i  3463  pwjust  3477  snjust  3498  dfpr2  3512  disjpr2  3553  difprsn1  3625  diftpsn3  3627  difpr  3628  dfuni2  3704  intab  3766  intunsn  3775  rint0  3776  iunid  3834  viin  3838  iinrabm  3841  2iunin  3845  riin0  3850  iunxprg  3859  unopab  3967  cbvmptf  3982  cbvmpt  3983  unisucg  4296  op1stb  4359  orddif  4422  elxpi  4515  csbxpg  4580  relopabi  4625  inxp  4633  coeq12i  4662  dfdm3  4686  dfrn3  4688  dmun  4706  dmopab  4710  dmopab3  4712  dmxpid  4720  dmxpin  4721  rnopab  4746  rnmpt  4747  rncoss  4767  rncoeq  4770  reseq12i  4775  resundi  4790  resindi  4792  resiun1  4796  resdmdfsn  4820  resopab  4821  mptresid  4831  dfima3  4842  imadisj  4859  ndmima  4874  mptcnv  4899  rnun  4905  rnuni  4908  imaundi  4909  inimass  4913  cnvxp  4915  rnxpm  4926  dminxp  4941  imainrect  4942  cnvcnv3  4946  dmpropg  4969  op1sta  4978  op2ndb  4980  op2nda  4981  resdmres  4988  mptpreima  4990  coundi  4998  coundir  4999  cocnvcnv1  5007  cores2  5009  dfdm2  5031  iotajust  5045  dfiota2  5047  funi  5113  funtp  5134  fntpg  5137  funcnvuni  5150  funcnvres  5154  imadiflem  5160  imadif  5161  imainlem  5162  imain  5163  fnresdisj  5191  mptfng  5206  resdif  5345  fv2  5370  dffv4g  5372  fveq12i  5381  nfvres  5408  0fv  5410  dfimafn2  5425  fnimapr  5435  fvmptss2  5450  fvmptg  5451  fvmpts  5453  fvmpt2  5458  mptfvex  5460  elfvmptrab  5470  fvopab6  5471  f1ompt  5525  dfmpt  5551  ressnop0  5555  fprg  5557  fvsnun1  5571  fsnunfv  5575  fvpr2g  5581  imauni  5616  fliftfuns  5653  cbvriota  5694  oveq123i  5742  fconstmpo  5820  resoprab  5821  mpofun  5827  rnmpo  5835  reldmmpo  5836  ov  5844  ovigg  5845  ovmpt4g  5847  ovg  5863  caov31  5914  elmpocl  5922  f1ocnvd  5926  oprabrexex2  5982  op1st  5998  op2nd  5999  f1stres  6011  f2ndres  6012  unielxp  6026  dfoprab3s  6042  dfoprab4  6044  mpompts  6050  mpofvex  6055  oprab2co  6069  df1st2  6070  df2nd2  6071  f1od2  6086  brtpos0  6103  tposoprab  6131  smores3  6144  tfrlemi14d  6184  tfr1onlemaccex  6199  tfrcllemaccex  6212  rdgisuc1  6235  rdg0  6238  frec0g  6248  df1o2  6280  df2o2  6282  oasuc  6314  omv2  6315  omsuc  6322  ecidsn  6430  qliftfuns  6467  oviec  6489  mapsncnv  6543  dfixp  6548  xpcomco  6673  xpassen  6677  ssenen  6698  undifdc  6765  unfiin  6767  fidcenumlemrks  6793  fidcenumlemr  6795  sbthlemi5  6801  sbthlemi8  6804  fi0  6815  inf00  6870  djuf1olemr  6891  djuinr  6900  djuin  6901  djuun  6904  casefun  6922  casedm  6923  caseinj  6926  caseinl  6928  caseinr  6929  endjusym  6933  eninl  6934  eninr  6935  djudm  6942  djuinj  6943  fodjuomni  6971  fodjumkv  6984  pm54.43  6996  exmidfodomrlemim  7005  xp2dju  7019  djucomen  7020  djuassen  7021  xpdjuen  7022  addpiord  7072  mulpiord  7073  dmaddpi  7081  dmmulpi  7082  recmulnqg  7147  1lt2nq  7162  halfnqq  7166  dfmq0qs  7185  dfplq0qs  7186  genpdf  7264  1prl  7311  1pru  7312  ltexprlemell  7354  ltexprlemelu  7355  recexprlemell  7378  recexprlemelu  7379  cauappcvgprlemm  7401  cauappcvgprlemopl  7402  cauappcvgprlemlol  7403  cauappcvgprlemopu  7404  cauappcvgprlemupu  7405  cauappcvgprlemdisj  7407  cauappcvgprlemloc  7408  cauappcvgprlemladdfu  7410  cauappcvgprlemladdfl  7411  cauappcvgprlemladdrl  7413  cauappcvgprlem2  7416  caucvgprlemm  7424  caucvgprlemopl  7425  caucvgprlemlol  7426  caucvgprlemopu  7427  caucvgprlemupu  7428  caucvgprlemdisj  7430  caucvgprlemloc  7431  caucvgprlemcl  7432  caucvgprlemladdfu  7433  caucvgprlemladdrl  7434  caucvgprlem2  7436  caucvgprprlemell  7441  caucvgprprlemelu  7442  caucvgprprlemml  7450  caucvgprprlemmu  7451  caucvgprprlemclphr  7461  caucvgprprlemexbt  7462  caucvgprprlem2  7466  addsrpr  7488  mulsrpr  7489  caucvgsrlemoffres  7542  caucvgsr  7544  addcnsr  7569  mulcnsr  7570  mulresr  7573  addvalex  7579  pitonnlem1  7580  axi2m1  7610  axcnre  7616  mulcomli  7697  mnfnre  7732  addcomli  7830  add42i  7851  mvrraddi  7902  neg0  7931  negdii  7969  negsubdi2i  7971  crap0  8626  2t2e4  8778  3t2e6  8780  3t3e9  8781  4t2e8  8782  neg1mulneg1e1  8836  8th4div3  8843  halfpm6th  8844  iap0  8847  dfdec10  9089  deceq12i  9094  numltc  9111  decsuc  9116  decsucc  9126  nummac  9130  numma2c  9131  numadd  9132  numaddc  9133  nummul1c  9134  nummul2c  9135  decma  9136  decmac  9137  decma2c  9138  decadd  9139  decaddc  9140  decrmanc  9142  decrmac  9143  decaddci  9146  decsubi  9148  decmul1  9149  decmul1c  9150  decmul2c  9151  11multnc  9153  4t3lem  9182  6t2e12  9189  7t2e14  9194  8t2e16  9200  9t2e18  9207  9t11e99  9215  divfnzn  9315  xnegpnf  9504  xneg0  9507  xaddmnf1  9524  xaddmnf2  9525  mnfaddpnf  9527  iooval2  9591  dfioo2  9650  fzval2  9686  fzsuc2  9752  fztpval  9756  fzo01  9886  fzo12sn  9887  fzo0to42pr  9890  fldiv4p1lem1div2  9971  intqfrac2  9985  intfracq  9986  1tonninf  10106  neg1sqe1  10280  sq2  10281  sq3  10282  cu2  10284  i2  10286  i3  10287  binom2i  10294  sq10  10352  3dec  10354  facp1  10369  fac2  10370  fac4  10372  4bc2eq6  10413  hashp1i  10449  pr0hash2ex  10454  hashfzo  10461  hashxp  10465  zfz1isolem1  10476  cji  10567  cnrecnv  10575  sqrt0  10668  resqrexlemover  10674  resqrexlemcalc3  10680  absi  10723  absimle  10748  sumeq12i  11026  summodclem2a  11042  summodc  11044  sum0  11049  fsumsplitf  11069  fsum2dlemstep  11095  fsumabs  11126  fsumiun  11138  0.999...  11182  mertenslem2  11197  ege2le3  11228  eft0val  11250  cos0  11288  cos1bnd  11317  cos2bnd  11318  3dvdsdec  11410  3dvds2dec  11411  odd2np1  11418  opoe  11440  nn0o  11452  gcd0val  11497  6gcd4e2  11529  3lcm2e6woprm  11613  3lcm2e6  11684  nn0gcdsq  11723  phiprmpw  11743  phimullem  11746  unennn  11755  ennnfonelemj0  11759  ennnfonelem0  11763  ennnfonelem1  11765  ennnfonelemhf1o  11771  ennnfonelemrn  11777  ennnfonelemdm  11778  strnfvnd  11822  slotslfn  11828  setsfun  11837  setsfun0  11838  setscom  11842  setsslid  11852  2strstr1g  11905  cnco  12232  txuni2  12267  txbas  12269  uptx  12285  txcn  12286  cnmptid  12292  cnmpt2t  12304  xmetxp  12496  cnmetdval  12518  remetdval  12525  resubmet  12534  rerestcntop  12536  divcnap  12541  ex-fl  12630  ex-exp  12632  ex-fac  12633  ex-bc  12634  ex-dvds  12635  ex-gcd  12636  bj-dfom  12821  pwle2  12883  exmid1stab  12885  nninfsellemqall  12901  isomninnlem  12915