Theorem eqtri 2255

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

Syntax hints:   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227

This theorem is referenced by:  eqtr2i  2256  eqtr3i  2257  eqtr4i  2258  3eqtri  2259  3eqtrri  2260  3eqtr2i  2261  cbvrab  2813  csb2  3143  cbvrabcsf  3207  difjust  3215  unjust  3217  injust  3219  dfdif3  3333  difeq12i  3339  ineqcomi  3417  inrot  3440  symdif1  3490  rabnc  3545  0in  3548  ssdifin0  3595  dfif3  3640  ifbieq2i  3650  ifbieq12i  3652  pwjust  3675  snjust  3699  dfpr2  3713  disjpr2  3758  rabsnifsb  3762  difprsn1  3838  diftpsn3  3840  difpr  3841  dfuni2  3921  intab  3983  intunsn  3992  rint0  3993  iunid  4052  viin  4056  iinrabm  4059  2iunin  4063  riin0  4068  iunxprg  4077  unopab  4194  cbvmptf  4209  cbvmpt  4210  exmid1stab  4326  unisucg  4540  op1stb  4604  orddif  4674  elxpi  4770  csbxpg  4836  relopabi  4885  inxp  4894  coeq12i  4923  dfdm3  4947  dfrn3  4949  dmun  4968  dmopab  4972  dmopab3  4974  dmxpid  4983  dmxpin  4984  rnopab  5009  rnmpt  5010  rncoss  5033  rncoeq  5036  reseq12i  5041  resundi  5056  resindi  5058  resiun1  5062  resdmdfsn  5086  resopab  5087  opabresid  5096  dfima3  5109  mptima  5118  imadisj  5129  ndmima  5144  mptcnv  5170  rnun  5176  rnuni  5179  imaundi  5180  inimass  5184  cnvxp  5186  rnxpm  5197  dminxp  5212  imainrect  5213  cnvcnv3  5217  dmpropg  5240  op1sta  5249  op2ndb  5251  op2nda  5252  resdmres  5259  mptpreima  5261  coundi  5269  coundir  5270  cocnvcnv1  5278  cores2  5280  dfdm2  5302  iotajust  5316  dfiota2  5318  funi  5389  funtp  5414  fntpg  5417  funcnvuni  5430  funcnvres  5434  imadiflem  5440  imadif  5441  imainlem  5442  imain  5443  fnresdisj  5473  mptfng  5489  fresaunres2disj  5550  resdif  5641  fv2  5670  dffv4g  5672  fveq12i  5681  nfvres  5711  0fv  5713  dfimafn2  5731  fnimapr  5742  fvmptss2  5757  fvmptg  5758  fvmpts  5760  fvmpt2  5766  mptfvex  5768  elfvmptrab  5778  fvopab6  5779  f1ompt  5833  dfmpt  5860  ressnop0  5870  fprg  5872  fvsnun1  5886  fsnunfv  5890  fvpr2g  5896  imauni  5940  fliftfuns  5977  cbvriota  6023  oveq123i  6072  fconstmpo  6156  resoprab  6157  mpofun  6163  rnmpo  6172  reldmmpo  6173  ov  6181  ovigg  6182  ovmpt4g  6184  ovg  6201  caov31  6252  elmpocl  6257  f1ocnvd  6265  oprabrexex2  6336  op1st  6353  op2nd  6354  f1stres  6366  f2ndres  6367  unielxp  6381  dfoprab3s  6397  dfoprab4  6399  mpompts  6407  mpofvex  6414  oprab2co  6427  df1st2  6428  df2nd2  6429  f1od2  6444  elmpom  6447  cnvimadfsn  6458  brtpos0  6496  tposoprab  6524  smores3  6537  tfrlemi14d  6577  tfr1onlemaccex  6592  tfrcllemaccex  6605  rdgisuc1  6628  rdg0  6631  frec0g  6641  df1o2  6674  df2o2  6676  oasuc  6710  omv2  6711  omsuc  6718  ecidsn  6829  qliftfuns  6866  oviec  6888  mapsncnv  6943  dfixp  6948  xpcomco  7090  xpassen  7094  ssenen  7118  undifdc  7197  unfiin  7199  fidcenumlemrks  7236  fidcenumlemr  7238  sbthlemi5  7244  sbthlemi8  7247  fi0  7275  inf00  7335  djuf1olemr  7358  djuinr  7367  djuin  7368  djuun  7371  casefun  7389  casedm  7390  caseinj  7393  caseinl  7395  caseinr  7396  endjusym  7400  eninl  7401  eninr  7402  djudm  7409  djuinj  7410  fodjuomni  7453  fodjumkv  7464  nninfwlporlemd  7476  pm54.43  7500  exmidfodomrlemim  7517  xp2dju  7535  djucomen  7536  djuassen  7537  xpdjuen  7538  pw1nel3  7554  sucpw1nel3  7556  addpiord  7647  mulpiord  7648  dmaddpi  7656  dmmulpi  7657  recmulnqg  7722  1lt2nq  7737  halfnqq  7741  dfmq0qs  7760  dfplq0qs  7761  genpdf  7839  1prl  7886  1pru  7887  ltexprlemell  7929  ltexprlemelu  7930  recexprlemell  7953  recexprlemelu  7954  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem2  8041  addsrpr  8076  mulsrpr  8077  caucvgsrlemoffres  8131  caucvgsr  8133  suplocsrlempr  8138  addcnsr  8165  mulcnsr  8166  mulresr  8169  addvalex  8175  pitonnlem1  8176  axi2m1  8206  axcnre  8212  mulcomli  8297  mnfnre  8332  addcomli  8434  add42i  8455  mvrraddi  8506  neg0  8535  negdii  8573  negsubdi2i  8575  crap0  9249  2t2e4  9409  3t2e6  9411  3t3e9  9412  4t2e8  9413  neg1mulneg1e1  9467  8th4div3  9474  halfpm6th  9475  iap0  9478  dfdec10  9730  deceq12i  9735  numltc  9752  decsuc  9757  decsucc  9767  nummac  9771  numma2c  9772  numadd  9773  numaddc  9774  nummul1c  9775  nummul2c  9776  decma  9777  decmac  9778  decma2c  9779  decadd  9780  decaddc  9781  decrmanc  9783  decrmac  9784  decaddci  9787  decsubi  9789  decmul1  9790  decmul1c  9791  decmul2c  9792  11multnc  9794  4t3lem  9823  6t2e12  9830  7t2e14  9835  8t2e16  9841  9t2e18  9848  9t11e99  9856  halfthird  9869  5recm6rec  9870  divfnzn  9971  xnegpnf  10180  xneg0  10183  xaddmnf1  10200  xaddmnf2  10201  mnfaddpnf  10203  iooval2  10267  dfioo2  10326  fzval2  10364  fzsuc2  10435  fztpval  10439  fz0to3un2pr  10479  fz0to4untppr  10480  fzo01  10583  fzo12sn  10584  fzo0to42pr  10587  fldiv4p1lem1div2  10689  intqfrac2  10705  intfracq  10706  xnn0nnen  10823  1tonninf  10827  neg1sqe1  11020  sq2  11021  sq3  11022  cu2  11024  i2  11026  i3  11027  binom2i  11034  sq10  11099  3dec  11101  facp1  11117  fac2  11118  fac4  11120  4bc2eq6  11162  hashp1i  11200  pr0hash2ex  11205  hashfzo  11212  hashxp  11216  hashfibclem  11231  zfz1isolem1  11237  elovmpowrd  11291  ccat1st1st  11354  cji  11612  cnrecnv  11620  sqrt0  11714  resqrexlemover  11720  resqrexlemcalc3  11726  absi  11769  absimle  11794  sumeq12i  12075  summodclem2a  12092  summodc  12094  sum0  12099  fsumsplitf  12119  fsum2dlemstep  12145  fsumabs  12176  fsumiun  12188  0.999...  12232  mertenslem2  12247  prodeq12i  12274  prodmodc  12289  fprod2dlemstep  12333  ege2le3  12382  eft0val  12404  cos0  12441  cos1bnd  12470  cos2bnd  12471  3dvdsdec  12576  3dvds2dec  12577  odd2np1  12584  opoe  12606  nn0o  12618  5ndvds3  12645  5ndvds6  12646  bitsfzolem  12665  m1bits  12671  gcd0val  12681  6gcd4e2  12716  nnmindc  12755  nnminle  12756  3lcm2e6woprm  12808  3lcm2e6  12882  nn0gcdsq  12922  phiprmpw  12944  phimullem  12947  pcprecl  13012  pcprendvds  13013  pcmptdvds  13068  pockthi  13081  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  4sqlem19  13132  dec5nprm  13137  dec2nprm  13138  modxai  13139  modsubi  13142  numexp2x  13148  decsplit0b  13149  decsplit0  13150  decsplit  13152  karatsuba  13153  2exp5  13155  2exp7  13157  2exp8  13158  2exp11  13159  2exp16  13160  3exp3  13161  ballotfilemelo  13166  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfval0  13179  ballotfileme  13180  ballotfilemi  13187  ballotfilemsval  13196  ballotfilemrval  13205  ballotfilemrinv  13221  ballotfilemth  13225  ballotfi  13226  unennn  13232  ennnfonelemj0  13236  ennnfonelem0  13240  ennnfonelem1  13242  ennnfonelemhf1o  13248  ennnfonelemrn  13254  ennnfonelemdm  13255  strnfvnd  13316  slotslfn  13322  setsfun  13331  setsfun0  13332  setscom  13336  setsslid  13347  2strstr1g  13419  eqglact  14026  ecqusaddd  14039  ghmeqker  14072  dfrhm2  14384  rmodislmod  14611  cnfldadd  14822  cnfldmul  14824  expghmap  14867  fczpsrbag  14932  cnco  15198  txuni2  15233  txbas  15235  uptx  15251  txcn  15252  cnmptid  15258  cnmpt2t  15270  xmetxp  15484  cnmetdval  15506  remetdval  15524  resubmet  15533  rerestcntop  15535  rerest  15537  divcnap  15542  cnrehmeocntop  15587  dvexp  15688  plyun0  15713  plyco  15736  plycj  15738  sinhalfpilem  15768  cosneghalfpi  15775  efhalfpi  15776  cospi  15777  efipi  15778  eulerid  15779  sin2pi  15780  cos2pi  15781  ef2pi  15782  sincosq4sgn  15806  cosq14gt0  15809  tangtx  15815  sincos4thpi  15817  sincos6thpi  15819  sinkpi  15824  cosq34lt1  15827  dfrelog  15837  2logb9irr  15948  2logb9irrALT  15951  2logb9irrap  15954  mersenne  15977  perfectlem2  15980  zabsle1  15984  lgslem2  15986  lgsfcl2  15991  lgsdir2lem1  16013  lgsdir2lem2  16014  lgsdir2lem4  16016  lgsdir2lem5  16017  lgseisen  16059  2lgslem3a  16078  2lgslem3b  16079  2lgslem3c  16080  2lgslem3d  16081  2lgs2  16087  2lgsoddprmlem3a  16092  2lgsoddprmlem3b  16093  2lgsoddprmlem3c  16094  2lgsoddprmlem3d  16095  pw0ss  16190  umgrislfupgrenlem  16237  vtxdgfval  16395  clwwlknon2  16541  clwwlknon2x  16542  eupth2lembfi  16584  konigsbergvtx  16589  konigsbergiedg  16590  konigsberglem1  16595  konigsberglem2  16596  konigsberglem3  16597  ex-fl  16605  ex-exp  16607  ex-fac  16608  ex-bc  16609  ex-dvds  16610  ex-gcd  16611  bj-dfom  16815  012of  16879  2o01f  16880  pwle2  16884  nninfsellemqall  16905  isomninnlem  16926  iswomninnlem  16946  ismkvnnlem  16949  dceqnconst  16958  dcapnconst  16959  taupi  16971  gfsump1  16980