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  6528  tposoprab  6556  smores3  6569  tfrlemi14d  6609  tfr1onlemaccex  6624  tfrcllemaccex  6637  rdgisuc1  6660  rdg0  6663  frec0g  6673  df1o2  6706  df2o2  6708  oasuc  6742  omv2  6743  omsuc  6750  ecidsn  6861  qliftfuns  6898  oviec  6920  mapsncnv  6983  dfixp  6988  xpcomco  7130  xpassen  7134  ssenen  7158  undifdc  7237  unfiin  7239  fidcenumlemrks  7277  fidcenumlemr  7279  sbthlemi5  7285  sbthlemi8  7288  fdmfifsupp  7301  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  9790  deceq12i  9795  numltc  9817  decsuc  9822  decsucc  9832  nummac  9836  numma2c  9837  numadd  9838  numaddc  9839  nummul1c  9840  nummul2c  9841  decma  9842  decmac  9843  decma2c  9844  decadd  9845  decaddc  9846  decrmanc  9848  decrmac  9849  decaddci  9852  decsubi  9854  decmul1  9855  decmul1c  9856  decmul2c  9857  11multnc  9859  4t3lem  9888  6t2e12  9895  7t2e14  9900  8t2e16  9906  9t2e18  9913  9t11e99  9921  halfthird  9934  5recm6rec  9935  divfnzn  10036  xnegpnf  10246  xneg0  10249  xaddmnf1  10266  xaddmnf2  10267  mnfaddpnf  10269  iooval2  10333  dfioo2  10392  fzval2  10430  fzsuc2  10502  fztpval  10506  fz0to3un2pr  10546  fz0to4untppr  10547  fzo01  10650  fzo12sn  10651  fzo0to42pr  10654  fldiv4p1lem1div2  10760  intqfrac2  10776  intfracq  10777  xnn0nnen  10894  1tonninf  10898  neg1sqe1  11091  sq2  11092  sq3  11093  cu2  11095  i2  11097  i3  11098  binom2i  11105  sq10  11171  3dec  11173  facp1  11189  fac2  11190  fac4  11192  4bc2eq6  11234  hashp1i  11272  pr0hash2ex  11277  hashfzo  11284  hashxp  11288  hashfibclem  11303  zfz1isolem1  11313  elovmpowrd  11367  ccat1st1st  11430  cji  11689  cnrecnv  11697  sqrt0  11791  resqrexlemover  11797  resqrexlemcalc3  11803  absi  11846  absimle  11872  sumeq12i  12155  summodclem2a  12172  summodc  12174  sum0  12179  fsumsplitf  12199  fsum2dlemstep  12225  fsumabs  12256  fsumiun  12268  0.999...  12312  mertenslem2  12327  prodeq12i  12354  prodmodc  12369  fprod2dlemstep  12413  ege2le3  12462  eft0val  12484  cos0  12521  cos1bnd  12550  cos2bnd  12551  3dvdsdec  12656  3dvds2dec  12657  odd2np1  12664  opoe  12686  nn0o  12698  5ndvds3  12725  5ndvds6  12726  bitsfzolem  12745  m1bits  12751  gcd0val  12761  6gcd4e2  12796  nnmindc  12835  nnminle  12836  3lcm2e6woprm  12888  3lcm2e6  12963  nn0gcdsq  13004  phiprmpw  13028  phimullem  13031  pcprecl  13096  pcprendvds  13097  pcmptdvds  13152  pockthi  13165  4sqlem13m  13210  4sqlem14  13211  4sqlem17  13214  4sqlem18  13215  4sqlem19  13216  dec5nprm  13221  dec2nprm  13222  modxai  13223  modsubi  13227  numexp2x  13233  decsplit0b  13234  decsplit0  13235  decsplit  13237  karatsuba  13238  2exp5  13240  2exp7  13242  2exp8  13243  2exp11  13244  2exp16  13245  3exp3  13246  prmlem0  13248  prmlem1  13250  5prm  13251  11prm  13257  prmlem2  13262  37prm  13263  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  ballotfilemelo  13279  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfval0  13292  ballotfileme  13293  ballotfilemi  13300  ballotfilemsval  13309  ballotfilemrval  13318  ballotfilemrinv  13334  ballotfilemth  13338  ballotfi  13339  unennn  13345  ennnfonelemj0  13349  ennnfonelem0  13353  ennnfonelem1  13355  ennnfonelemhf1o  13361  ennnfonelemrn  13367  ennnfonelemdm  13368  strnfvnd  13429  slotslfn  13435  setsfun  13444  setsfun0  13445  setscom  13449  setsslid  13460  2strstr1g  13534  eqglact  14086  ecqusaddd  14099  ghmeqker  14132  gsumsnfdcmn  14256  gsum2dfilem2  14271  gsum2d2fi  14273  dfrhm2  14569  rmodislmod  14796  cnfldadd  15007  cnfldmul  15009  gsumfsum  15031  expghmap  15050  asclfval  15129  fczpsrbag  15169  psrass1filem  15186  cnco  15464  txuni2  15499  txbas  15501  uptx  15517  txcn  15518  cnmptid  15524  cnmpt2t  15536  xmetxp  15750  cnmetdval  15772  remetdval  15790  resubmet  15799  rerestcntop  15801  rerest  15803  divcnap  15808  cnrehmeocntop  15853  dvexp  15954  plyun0  15979  plyco  16002  plycj  16004  sinhalfpilem  16035  cosneghalfpi  16042  efhalfpi  16043  cospi  16044  efipi  16045  eulerid  16046  sin2pi  16047  cos2pi  16048  ef2pi  16049  sincosq4sgn  16073  cosq14gt0  16076  tangtx  16082  sincos4thpi  16084  sincos6thpi  16086  sinkpi  16091  cosq34lt1  16095  dfrelog  16106  2logb9irr  16224  2logb9irrALT  16227  2logb9irrap  16230  log2tlbndlog2  16237  log2ublem2  16239  log2ublem3  16240  log2ublog2  16241  birthdaylem2  16243  birthdaylog2  16245  ppi1  16287  cht1  16288  ppiqub  16310  chtqub  16313  mersenne  16314  perfectlem2  16317  bcp1ctr  16323  bclbnd  16324  bposlem6  16333  bposlem8  16335  bposlem9  16336  zabsle1  16340  lgslem2  16342  lgsfcl2  16347  lgsdir2lem1  16369  lgsdir2lem2  16370  lgsdir2lem4  16372  lgsdir2lem5  16373  lgseisen  16415  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgs2  16443  2lgsoddprmlem3a  16448  2lgsoddprmlem3b  16449  2lgsoddprmlem3c  16450  2lgsoddprmlem3d  16451  pw0ss  16546  umgrislfupgrenlem  16593  vtxdgfval  16751  clwwlknon2  16897  clwwlknon2x  16898  eupth2lembfi  16940  konigsbergvtx  16945  konigsbergiedg  16946  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  ex-fl  16961  ex-exp  16963  ex-fac  16964  ex-bc  16965  ex-dvds  16966  ex-gcd  16967  bj-dfom  17181  012of  17245  2o01f  17246  pwle2  17250  nninfsellemqall  17281  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326  dceqnconst  17334  dcapnconst  17335  taupi  17347