Theorem eqtri 2259

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2i  2260  eqtr3i  2261  eqtr4i  2262  3eqtri  2263  3eqtrri  2264  3eqtr2i  2265  cbvrab  2819  csb2  3149  cbvrabcsf  3213  difjust  3221  unjust  3223  injust  3225  dfdif3  3339  difeq12i  3345  ineqcomi  3423  inrot  3446  symdif1  3496  rabnc  3555  0in  3558  ssdifin0  3609  dfif3  3654  ifbieq2i  3664  ifbieq12i  3666  pwjust  3689  snjust  3714  dfpr2  3728  disjpr2  3773  rabsnifsb  3777  difprsn1  3854  diftpsn3  3856  difpr  3857  dfuni2  3937  intab  3999  intunsn  4008  rint0  4009  iunid  4068  viin  4072  iinrabm  4075  2iunin  4079  riin0  4084  iunxprg  4093  unopab  4211  cbvmptf  4227  cbvmpt  4228  exmid1stab  4347  unisucg  4561  op1stb  4626  orddif  4696  elxpi  4792  csbxpg  4858  relopabi  4907  inxp  4916  coeq12i  4945  dfdm3  4969  dfrn3  4971  dmun  4990  dmopab  4994  dmopab3  4996  dmxpid  5005  dmxpin  5006  rnopab  5031  rnmpt  5032  rncoss  5055  rncoeq  5058  reseq12i  5063  resundi  5078  resindi  5080  resiun1  5084  resdmdfsn  5109  resopab  5110  opabresid  5119  dfima3  5132  mptima  5141  imadisj  5152  ndmima  5167  mptcnv  5193  rnun  5199  rnuni  5202  imaundi  5203  inimass  5207  cnvxp  5209  rnxpm  5220  dminxp  5235  imainrect  5236  cnvcnv3  5240  dmpropg  5263  op1sta  5272  op2ndb  5274  op2nda  5275  resdmres  5282  mptpreima  5284  coundi  5292  coundir  5293  cocnvcnv1  5301  cores2  5303  dfdm2  5325  iotajust  5339  dfiota2  5341  funi  5412  funtp  5437  fntpg  5440  funcnvuni  5453  funcnvres  5457  imadiflem  5463  imadif  5464  imainlem  5465  imain  5466  fnresdisj  5496  mptfng  5512  fresaunres2disj  5573  resdif  5664  fv2  5693  dffv4g  5695  fveq12i  5704  nfvres  5735  0fv  5737  dfimafn2  5755  fnimapr  5766  fvmptss2  5783  fvmptg  5784  fvmpts  5786  fvmpt2  5792  mptfvex  5794  elfvmptrab  5805  fvmptndm  5807  fvopab6  5808  f1ompt  5862  dfmpt  5889  ressnop0  5899  fprg  5901  fvsnun1  5915  fsnunfv  5919  fvpr2g  5925  imauni  5970  fliftfuns  6007  cbvriota  6053  oveq123i  6102  fconstmpo  6186  resoprab  6187  mpofun  6193  rnmpo  6202  reldmmpo  6203  ov  6211  ovigg  6212  ovmpt4g  6214  ovg  6231  caov31  6282  elmpocl  6287  f1ocnvd  6295  oprabrexex2  6367  op1st  6384  op2nd  6385  f1stres  6397  f2ndres  6398  unielxp  6412  dfoprab3s  6428  dfoprab4  6430  mpompts  6438  mpofvex  6445  oprab2co  6458  df1st2  6459  df2nd2  6460  f1od2  6475  elmpom  6478  cnvimadfsn  6489  brtpos0  6527  tposoprab  6555  smores3  6568  tfrlemi14d  6608  tfr1onlemaccex  6623  tfrcllemaccex  6636  rdgisuc1  6659  rdg0  6662  frec0g  6672  df1o2  6705  df2o2  6707  oasuc  6741  omv2  6742  omsuc  6749  ecidsn  6860  qliftfuns  6897  oviec  6919  mapsncnv  6982  dfixp  6987  xpcomco  7129  xpassen  7133  ssenen  7157  undifdc  7236  unfiin  7238  fidcenumlemrks  7276  fidcenumlemr  7278  sbthlemi5  7284  sbthlemi8  7287  fi0  7315  inf00  7378  djuf1olemr  7401  djuinr  7410  djuin  7411  djuun  7414  casefun  7432  casedm  7433  caseinj  7436  caseinl  7438  caseinr  7439  endjusym  7443  eninl  7444  eninr  7445  djudm  7452  djuinj  7453  fodjuomni  7496  fodjumkv  7507  nninfwlporlemd  7519  pm54.43  7543  exmidfodomrlemim  7560  xp2dju  7578  djucomen  7579  djuassen  7580  xpdjuen  7581  pw1nel3  7597  sucpw1nel3  7599  addpiord  7690  mulpiord  7691  dmaddpi  7699  dmmulpi  7700  recmulnqg  7765  1lt2nq  7780  halfnqq  7784  dfmq0qs  7803  dfplq0qs  7804  genpdf  7882  1prl  7929  1pru  7930  ltexprlemell  7972  ltexprlemelu  7973  recexprlemell  7996  recexprlemelu  7997  cauappcvgprlemm  8019  cauappcvgprlemopl  8020  cauappcvgprlemlol  8021  cauappcvgprlemopu  8022  cauappcvgprlemupu  8023  cauappcvgprlemdisj  8025  cauappcvgprlemloc  8026  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  cauappcvgprlemladdrl  8031  cauappcvgprlem2  8034  caucvgprlemm  8042  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemopu  8045  caucvgprlemupu  8046  caucvgprlemdisj  8048  caucvgprlemloc  8049  caucvgprlemcl  8050  caucvgprlemladdfu  8051  caucvgprlemladdrl  8052  caucvgprlem2  8054  caucvgprprlemell  8059  caucvgprprlemelu  8060  caucvgprprlemml  8068  caucvgprprlemmu  8069  caucvgprprlemclphr  8079  caucvgprprlemexbt  8080  caucvgprprlem2  8084  addsrpr  8119  mulsrpr  8120  caucvgsrlemoffres  8174  caucvgsr  8176  suplocsrlempr  8181  addcnsr  8208  mulcnsr  8209  mulresr  8212  addvalex  8218  pitonnlem1  8219  axi2m1  8249  axcnre  8255  mulcomli  8340  mnfnre  8375  addcomli  8479  add42i  8500  mvrraddi  8551  neg0  8580  negdii  8618  negsubdi2i  8620  crap0  9297  2t2e4  9469  3t2e6  9471  3t3e9  9473  4t2e8  9474  neg1mulneg1e1  9529  8th4div3  9536  halfpm6th  9537  iap0  9540  dfdec10  9792  deceq12i  9797  numltc  9819  decsuc  9824  decsucc  9834  nummac  9838  numma2c  9839  numadd  9840  numaddc  9841  nummul1c  9842  nummul2c  9843  decma  9844  decmac  9845  decma2c  9846  decadd  9847  decaddc  9848  decrmanc  9850  decrmac  9851  decaddci  9854  decsubi  9856  decmul1  9857  decmul1c  9858  decmul2c  9859  11multnc  9861  4t3lem  9890  6t2e12  9897  7t2e14  9902  8t2e16  9908  9t2e18  9915  9t11e99  9923  halfthird  9936  5recm6rec  9937  divfnzn  10038  xnegpnf  10248  xneg0  10251  xaddmnf1  10268  xaddmnf2  10269  mnfaddpnf  10271  iooval2  10335  dfioo2  10394  fzval2  10432  fzsuc2  10504  fztpval  10508  fz0to3un2pr  10548  fz0to4untppr  10549  fzo01  10652  fzo12sn  10653  fzo0to42pr  10656  fldiv4p1lem1div2  10762  intqfrac2  10778  intfracq  10779  xnn0nnen  10896  1tonninf  10900  neg1sqe1  11093  sq2  11094  sq3  11095  cu2  11097  i2  11099  i3  11100  binom2i  11107  sq10  11173  3dec  11175  facp1  11191  fac2  11192  fac4  11194  4bc2eq6  11236  hashp1i  11274  pr0hash2ex  11279  hashfzo  11286  hashxp  11290  hashfibclem  11305  zfz1isolem1  11315  elovmpowrd  11369  ccat1st1st  11432  cji  11691  cnrecnv  11699  sqrt0  11793  resqrexlemover  11799  resqrexlemcalc3  11805  absi  11848  absimle  11874  sumeq12i  12157  summodclem2a  12174  summodc  12176  sum0  12181  fsumsplitf  12201  fsum2dlemstep  12227  fsumabs  12258  fsumiun  12270  0.999...  12314  mertenslem2  12329  prodeq12i  12356  prodmodc  12371  fprod2dlemstep  12415  ege2le3  12464  eft0val  12486  cos0  12523  cos1bnd  12552  cos2bnd  12553  3dvdsdec  12658  3dvds2dec  12659  odd2np1  12666  opoe  12688  nn0o  12700  5ndvds3  12727  5ndvds6  12728  bitsfzolem  12747  m1bits  12753  gcd0val  12763  6gcd4e2  12798  nnmindc  12837  nnminle  12838  3lcm2e6woprm  12890  3lcm2e6  12965  nn0gcdsq  13006  phiprmpw  13030  phimullem  13033  pcprecl  13098  pcprendvds  13099  pcmptdvds  13154  pockthi  13167  4sqlem13m  13212  4sqlem14  13213  4sqlem17  13216  4sqlem18  13217  4sqlem19  13218  dec5nprm  13223  dec2nprm  13224  modxai  13225  modsubi  13229  numexp2x  13235  decsplit0b  13236  decsplit0  13237  decsplit  13239  karatsuba  13240  2exp5  13242  2exp7  13244  2exp8  13245  2exp11  13246  2exp16  13247  3exp3  13248  prmlem0  13250  prmlem1  13252  5prm  13253  11prm  13259  prmlem2  13264  37prm  13265  43prm  13266  83prm  13267  139prm  13268  163prm  13269  317prm  13270  631prm  13271  1259lem1  13272  1259lem2  13273  1259lem3  13274  1259lem4  13275  1259lem5  13276  1259prm  13277  ballotfilemelo  13281  ballotfilem2  13287  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemfval0  13294  ballotfileme  13295  ballotfilemi  13302  ballotfilemsval  13311  ballotfilemrval  13320  ballotfilemrinv  13336  ballotfilemth  13340  ballotfi  13341  unennn  13347  ennnfonelemj0  13351  ennnfonelem0  13355  ennnfonelem1  13357  ennnfonelemhf1o  13363  ennnfonelemrn  13369  ennnfonelemdm  13370  strnfvnd  13431  slotslfn  13437  setsfun  13446  setsfun0  13447  setscom  13451  setsslid  13462  2strstr1g  13536  eqglact  14088  ecqusaddd  14101  ghmeqker  14134  gsumsnfdcmn  14258  gsum2dfilem2  14273  gsum2d2fi  14275  dfrhm2  14571  rmodislmod  14798  cnfldadd  15009  cnfldmul  15011  gsumfsum  15033  expghmap  15052  asclfval  15131  fczpsrbag  15171  psrass1filem  15182  cnco  15459  txuni2  15494  txbas  15496  uptx  15512  txcn  15513  cnmptid  15519  cnmpt2t  15531  xmetxp  15745  cnmetdval  15767  remetdval  15785  resubmet  15794  rerestcntop  15796  rerest  15798  divcnap  15803  cnrehmeocntop  15848  dvexp  15949  plyun0  15974  plyco  15997  plycj  15999  sinhalfpilem  16030  cosneghalfpi  16037  efhalfpi  16038  cospi  16039  efipi  16040  eulerid  16041  sin2pi  16042  cos2pi  16043  ef2pi  16044  sincosq4sgn  16068  cosq14gt0  16071  tangtx  16077  sincos4thpi  16079  sincos6thpi  16081  sinkpi  16086  cosq34lt1  16090  dfrelog  16101  2logb9irr  16219  2logb9irrALT  16222  2logb9irrap  16225  log2tlbndlog2  16232  log2ublem2  16234  log2ublem3  16235  log2ublog2  16236  birthdaylem2  16238  birthdaylog2  16240  ppi1  16282  cht1  16283  ppiqub  16305  chtqub  16308  mersenne  16309  perfectlem2  16312  bcp1ctr  16318  bclbnd  16319  bposlem6  16328  bposlem8  16330  bposlem9  16331  zabsle1  16335  lgslem2  16337  lgsfcl2  16342  lgsdir2lem1  16364  lgsdir2lem2  16365  lgsdir2lem4  16367  lgsdir2lem5  16368  lgseisen  16410  2lgslem3a  16429  2lgslem3b  16430  2lgslem3c  16431  2lgslem3d  16432  2lgs2  16438  2lgsoddprmlem3a  16443  2lgsoddprmlem3b  16444  2lgsoddprmlem3c  16445  2lgsoddprmlem3d  16446  pw0ss  16541  umgrislfupgrenlem  16588  vtxdgfval  16746  clwwlknon2  16892  clwwlknon2x  16893  eupth2lembfi  16935  konigsbergvtx  16940  konigsbergiedg  16941  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  ex-fl  16956  ex-exp  16958  ex-fac  16959  ex-bc  16960  ex-dvds  16961  ex-gcd  16962  bj-dfom  17176  012of  17240  2o01f  17241  pwle2  17245  nninfsellemqall  17276  isomninnlem  17297  iswomninnlem  17318  ismkvnnlem  17321  dceqnconst  17329  dcapnconst  17330  taupi  17342