Theorem eqtri 2259

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

Hypotheses

Ref	Expression
eqtri.1	|- A = B
eqtri.2	|- B = C

Assertion

Ref	Expression
eqtri	|- A = C

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 |- A = B
2		eqtri.2	. . 3 |- B = C
3	2	eqeq2i 2249	. 2 |- ( A = B <-> A = C )
4	1, 3	mpbi 145	1 |- A = C

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  6981  dfixp  6986  xpcomco  7128  xpassen  7132  ssenen  7156  undifdc  7235  unfiin  7237  fidcenumlemrks  7275  fidcenumlemr  7277  sbthlemi5  7283  sbthlemi8  7286  fi0  7314  inf00  7377  djuf1olemr  7400  djuinr  7409  djuin  7410  djuun  7413  casefun  7431  casedm  7432  caseinj  7435  caseinl  7437  caseinr  7438  endjusym  7442  eninl  7443  eninr  7444  djudm  7451  djuinj  7452  fodjuomni  7495  fodjumkv  7506  nninfwlporlemd  7518  pm54.43  7542  exmidfodomrlemim  7559  xp2dju  7577  djucomen  7578  djuassen  7579  xpdjuen  7580  pw1nel3  7596  sucpw1nel3  7598  addpiord  7689  mulpiord  7690  dmaddpi  7698  dmmulpi  7699  recmulnqg  7764  1lt2nq  7779  halfnqq  7783  dfmq0qs  7802  dfplq0qs  7803  genpdf  7881  1prl  7928  1pru  7929  ltexprlemell  7971  ltexprlemelu  7972  recexprlemell  7995  recexprlemelu  7996  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem2  8053  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemclphr  8078  caucvgprprlemexbt  8079  caucvgprprlem2  8083  addsrpr  8118  mulsrpr  8119  caucvgsrlemoffres  8173  caucvgsr  8175  suplocsrlempr  8180  addcnsr  8207  mulcnsr  8208  mulresr  8211  addvalex  8217  pitonnlem1  8218  axi2m1  8248  axcnre  8254  mulcomli  8339  mnfnre  8374  addcomli  8478  add42i  8499  mvrraddi  8550  neg0  8579  negdii  8617  negsubdi2i  8619  crap0  9296  2t2e4  9468  3t2e6  9470  3t3e9  9472  4t2e8  9473  neg1mulneg1e1  9528  8th4div3  9535  halfpm6th  9536  iap0  9539  dfdec10  9791  deceq12i  9796  numltc  9818  decsuc  9823  decsucc  9833  nummac  9837  numma2c  9838  numadd  9839  numaddc  9840  nummul1c  9841  nummul2c  9842  decma  9843  decmac  9844  decma2c  9845  decadd  9846  decaddc  9847  decrmanc  9849  decrmac  9850  decaddci  9853  decsubi  9855  decmul1  9856  decmul1c  9857  decmul2c  9858  11multnc  9860  4t3lem  9889  6t2e12  9896  7t2e14  9901  8t2e16  9907  9t2e18  9914  9t11e99  9922  halfthird  9935  5recm6rec  9936  divfnzn  10037  xnegpnf  10247  xneg0  10250  xaddmnf1  10267  xaddmnf2  10268  mnfaddpnf  10270  iooval2  10334  dfioo2  10393  fzval2  10431  fzsuc2  10503  fztpval  10507  fz0to3un2pr  10547  fz0to4untppr  10548  fzo01  10651  fzo12sn  10652  fzo0to42pr  10655  fldiv4p1lem1div2  10761  intqfrac2  10777  intfracq  10778  xnn0nnen  10895  1tonninf  10899  neg1sqe1  11092  sq2  11093  sq3  11094  cu2  11096  i2  11098  i3  11099  binom2i  11106  sq10  11172  3dec  11174  facp1  11190  fac2  11191  fac4  11193  4bc2eq6  11235  hashp1i  11273  pr0hash2ex  11278  hashfzo  11285  hashxp  11289  hashfibclem  11304  zfz1isolem1  11314  elovmpowrd  11368  ccat1st1st  11431  cji  11690  cnrecnv  11698  sqrt0  11792  resqrexlemover  11798  resqrexlemcalc3  11804  absi  11847  absimle  11873  sumeq12i  12156  summodclem2a  12173  summodc  12175  sum0  12180  fsumsplitf  12200  fsum2dlemstep  12226  fsumabs  12257  fsumiun  12269  0.999...  12313  mertenslem2  12328  prodeq12i  12355  prodmodc  12370  fprod2dlemstep  12414  ege2le3  12463  eft0val  12485  cos0  12522  cos1bnd  12551  cos2bnd  12552  3dvdsdec  12657  3dvds2dec  12658  odd2np1  12665  opoe  12687  nn0o  12699  5ndvds3  12726  5ndvds6  12727  bitsfzolem  12746  m1bits  12752  gcd0val  12762  6gcd4e2  12797  nnmindc  12836  nnminle  12837  3lcm2e6woprm  12889  3lcm2e6  12964  nn0gcdsq  13005  phiprmpw  13029  phimullem  13032  pcprecl  13097  pcprendvds  13098  pcmptdvds  13153  pockthi  13166  4sqlem13m  13211  4sqlem14  13212  4sqlem17  13215  4sqlem18  13216  4sqlem19  13217  dec5nprm  13222  dec2nprm  13223  modxai  13224  modsubi  13228  numexp2x  13234  decsplit0b  13235  decsplit0  13236  decsplit  13238  karatsuba  13239  2exp5  13241  2exp7  13243  2exp8  13244  2exp11  13245  2exp16  13246  3exp3  13247  prmlem0  13249  prmlem1  13251  5prm  13252  11prm  13258  prmlem2  13263  37prm  13264  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilemelo  13280  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfval0  13293  ballotfileme  13294  ballotfilemi  13301  ballotfilemsval  13310  ballotfilemrval  13319  ballotfilemrinv  13335  ballotfilemth  13339  ballotfi  13340  unennn  13346  ennnfonelemj0  13350  ennnfonelem0  13354  ennnfonelem1  13356  ennnfonelemhf1o  13362  ennnfonelemrn  13368  ennnfonelemdm  13369  strnfvnd  13430  slotslfn  13436  setsfun  13445  setsfun0  13446  setscom  13450  setsslid  13461  2strstr1g  13535  eqglact  14087  ecqusaddd  14100  ghmeqker  14133  gsumsnfdcmn  14257  gsum2dfilem2  14272  gsum2d2fi  14274  dfrhm2  14570  rmodislmod  14797  cnfldadd  15008  cnfldmul  15010  gsumfsum  15032  expghmap  15051  asclfval  15130  fczpsrbag  15165  psrass1filem  15177  cnco  15447  txuni2  15482  txbas  15484  uptx  15500  txcn  15501  cnmptid  15507  cnmpt2t  15519  xmetxp  15733  cnmetdval  15755  remetdval  15773  resubmet  15782  rerestcntop  15784  rerest  15786  divcnap  15791  cnrehmeocntop  15836  dvexp  15937  plyun0  15962  plyco  15985  plycj  15987  sinhalfpilem  16018  cosneghalfpi  16025  efhalfpi  16026  cospi  16027  efipi  16028  eulerid  16029  sin2pi  16030  cos2pi  16031  ef2pi  16032  sincosq4sgn  16056  cosq14gt0  16059  tangtx  16065  sincos4thpi  16067  sincos6thpi  16069  sinkpi  16074  cosq34lt1  16078  dfrelog  16089  2logb9irr  16207  2logb9irrALT  16210  2logb9irrap  16213  log2tlbndlog2  16220  log2ublem2  16222  log2ublem3  16223  log2ublog2  16224  birthdaylem2  16226  birthdaylog2  16228  ppi1  16270  cht1  16271  ppiqub  16293  chtqub  16296  mersenne  16297  perfectlem2  16300  bcp1ctr  16306  bclbnd  16307  bposlem6  16316  bposlem8  16318  bposlem9  16319  zabsle1  16323  lgslem2  16325  lgsfcl2  16330  lgsdir2lem1  16352  lgsdir2lem2  16353  lgsdir2lem4  16355  lgsdir2lem5  16356  lgseisen  16398  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgs2  16426  2lgsoddprmlem3a  16431  2lgsoddprmlem3b  16432  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434  pw0ss  16529  umgrislfupgrenlem  16576  vtxdgfval  16734  clwwlknon2  16880  clwwlknon2x  16881  eupth2lembfi  16923  konigsbergvtx  16928  konigsbergiedg  16929  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  ex-fl  16944  ex-exp  16946  ex-fac  16947  ex-bc  16948  ex-dvds  16949  ex-gcd  16950  bj-dfom  17164  012of  17228  2o01f  17229  pwle2  17233  nninfsellemqall  17264  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309  dceqnconst  17317  dcapnconst  17318  taupi  17330