Theorem eqtri 2161

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 2151	. 2 |- ( A = B <-> A = C )
4	1, 3	mpbi 144	1 |- A = C

Syntax hints:   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  eqtr2i  2162  eqtr3i  2163  eqtr4i  2164  3eqtri  2165  3eqtrri  2166  3eqtr2i  2167  cbvrab  2687  csb2  3009  cbvrabcsf  3070  difjust  3077  unjust  3079  injust  3081  dfdif3  3191  difeq12i  3197  inrot  3296  symdif1  3346  rabnc  3400  0in  3403  ssdifin0  3449  dfif3  3492  ifbieq2i  3500  ifbieq12i  3502  pwjust  3516  snjust  3537  dfpr2  3551  disjpr2  3595  difprsn1  3667  diftpsn3  3669  difpr  3670  dfuni2  3746  intab  3808  intunsn  3817  rint0  3818  iunid  3876  viin  3880  iinrabm  3883  2iunin  3887  riin0  3892  iunxprg  3901  unopab  4015  cbvmptf  4030  cbvmpt  4031  unisucg  4344  op1stb  4407  orddif  4470  elxpi  4563  csbxpg  4628  relopabi  4673  inxp  4681  coeq12i  4710  dfdm3  4734  dfrn3  4736  dmun  4754  dmopab  4758  dmopab3  4760  dmxpid  4768  dmxpin  4769  rnopab  4794  rnmpt  4795  rncoss  4817  rncoeq  4820  reseq12i  4825  resundi  4840  resindi  4842  resiun1  4846  resdmdfsn  4870  resopab  4871  mptresid  4881  dfima3  4892  imadisj  4909  ndmima  4924  mptcnv  4949  rnun  4955  rnuni  4958  imaundi  4959  inimass  4963  cnvxp  4965  rnxpm  4976  dminxp  4991  imainrect  4992  cnvcnv3  4996  dmpropg  5019  op1sta  5028  op2ndb  5030  op2nda  5031  resdmres  5038  mptpreima  5040  coundi  5048  coundir  5049  cocnvcnv1  5057  cores2  5059  dfdm2  5081  iotajust  5095  dfiota2  5097  funi  5163  funtp  5184  fntpg  5187  funcnvuni  5200  funcnvres  5204  imadiflem  5210  imadif  5211  imainlem  5212  imain  5213  fnresdisj  5241  mptfng  5256  resdif  5397  fv2  5424  dffv4g  5426  fveq12i  5435  nfvres  5462  0fv  5464  dfimafn2  5479  fnimapr  5489  fvmptss2  5504  fvmptg  5505  fvmpts  5507  fvmpt2  5512  mptfvex  5514  elfvmptrab  5524  fvopab6  5525  f1ompt  5579  dfmpt  5605  ressnop0  5609  fprg  5611  fvsnun1  5625  fsnunfv  5629  fvpr2g  5635  imauni  5670  fliftfuns  5707  cbvriota  5748  oveq123i  5796  fconstmpo  5874  resoprab  5875  mpofun  5881  rnmpo  5889  reldmmpo  5890  ov  5898  ovigg  5899  ovmpt4g  5901  ovg  5917  caov31  5968  elmpocl  5976  f1ocnvd  5980  oprabrexex2  6036  op1st  6052  op2nd  6053  f1stres  6065  f2ndres  6066  unielxp  6080  dfoprab3s  6096  dfoprab4  6098  mpompts  6104  mpofvex  6109  oprab2co  6123  df1st2  6124  df2nd2  6125  f1od2  6140  brtpos0  6157  tposoprab  6185  smores3  6198  tfrlemi14d  6238  tfr1onlemaccex  6253  tfrcllemaccex  6266  rdgisuc1  6289  rdg0  6292  frec0g  6302  df1o2  6334  df2o2  6336  oasuc  6368  omv2  6369  omsuc  6376  ecidsn  6484  qliftfuns  6521  oviec  6543  mapsncnv  6597  dfixp  6602  xpcomco  6728  xpassen  6732  ssenen  6753  undifdc  6820  unfiin  6822  fidcenumlemrks  6849  fidcenumlemr  6851  sbthlemi5  6857  sbthlemi8  6860  fi0  6871  inf00  6926  djuf1olemr  6947  djuinr  6956  djuin  6957  djuun  6960  casefun  6978  casedm  6979  caseinj  6982  caseinl  6984  caseinr  6985  endjusym  6989  eninl  6990  eninr  6991  djudm  6998  djuinj  6999  fodjuomni  7029  fodjumkv  7042  pm54.43  7063  exmidfodomrlemim  7074  xp2dju  7088  djucomen  7089  djuassen  7090  xpdjuen  7091  addpiord  7148  mulpiord  7149  dmaddpi  7157  dmmulpi  7158  recmulnqg  7223  1lt2nq  7238  halfnqq  7242  dfmq0qs  7261  dfplq0qs  7262  genpdf  7340  1prl  7387  1pru  7388  ltexprlemell  7430  ltexprlemelu  7431  recexprlemell  7454  recexprlemelu  7455  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdrl  7489  cauappcvgprlem2  7492  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem2  7512  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  caucvgprprlem2  7542  addsrpr  7577  mulsrpr  7578  caucvgsrlemoffres  7632  caucvgsr  7634  suplocsrlempr  7639  addcnsr  7666  mulcnsr  7667  mulresr  7670  addvalex  7676  pitonnlem1  7677  axi2m1  7707  axcnre  7713  mulcomli  7797  mnfnre  7832  addcomli  7931  add42i  7952  mvrraddi  8003  neg0  8032  negdii  8070  negsubdi2i  8072  crap0  8740  2t2e4  8898  3t2e6  8900  3t3e9  8901  4t2e8  8902  neg1mulneg1e1  8956  8th4div3  8963  halfpm6th  8964  iap0  8967  dfdec10  9209  deceq12i  9214  numltc  9231  decsuc  9236  decsucc  9246  nummac  9250  numma2c  9251  numadd  9252  numaddc  9253  nummul1c  9254  nummul2c  9255  decma  9256  decmac  9257  decma2c  9258  decadd  9259  decaddc  9260  decrmanc  9262  decrmac  9263  decaddci  9266  decsubi  9268  decmul1  9269  decmul1c  9270  decmul2c  9271  11multnc  9273  4t3lem  9302  6t2e12  9309  7t2e14  9314  8t2e16  9320  9t2e18  9327  9t11e99  9335  halfthird  9348  5recm6rec  9349  divfnzn  9440  xnegpnf  9641  xneg0  9644  xaddmnf1  9661  xaddmnf2  9662  mnfaddpnf  9664  iooval2  9728  dfioo2  9787  fzval2  9824  fzsuc2  9890  fztpval  9894  fzo01  10024  fzo12sn  10025  fzo0to42pr  10028  fldiv4p1lem1div2  10109  intqfrac2  10123  intfracq  10124  1tonninf  10244  neg1sqe1  10418  sq2  10419  sq3  10420  cu2  10422  i2  10424  i3  10425  binom2i  10432  sq10  10490  3dec  10492  facp1  10508  fac2  10509  fac4  10511  4bc2eq6  10552  hashp1i  10588  pr0hash2ex  10593  hashfzo  10600  hashxp  10604  zfz1isolem1  10615  cji  10706  cnrecnv  10714  sqrt0  10808  resqrexlemover  10814  resqrexlemcalc3  10820  absi  10863  absimle  10888  sumeq12i  11166  summodclem2a  11182  summodc  11184  sum0  11189  fsumsplitf  11209  fsum2dlemstep  11235  fsumabs  11266  fsumiun  11278  0.999...  11322  mertenslem2  11337  prodeq12i  11364  prodmodc  11379  ege2le3  11414  eft0val  11436  cos0  11473  cos1bnd  11502  cos2bnd  11503  3dvdsdec  11598  3dvds2dec  11599  odd2np1  11606  opoe  11628  nn0o  11640  gcd0val  11685  6gcd4e2  11719  3lcm2e6woprm  11803  3lcm2e6  11874  nn0gcdsq  11914  phiprmpw  11934  phimullem  11937  unennn  11946  ennnfonelemj0  11950  ennnfonelem0  11954  ennnfonelem1  11956  ennnfonelemhf1o  11962  ennnfonelemrn  11968  ennnfonelemdm  11969  strnfvnd  12018  slotslfn  12024  setsfun  12033  setsfun0  12034  setscom  12038  setsslid  12048  2strstr1g  12101  cnco  12429  txuni2  12464  txbas  12466  uptx  12482  txcn  12483  cnmptid  12489  cnmpt2t  12501  xmetxp  12715  cnmetdval  12737  remetdval  12747  resubmet  12756  rerestcntop  12758  divcnap  12763  cnrehmeocntop  12801  dvexp  12883  sinhalfpilem  12920  cosneghalfpi  12927  efhalfpi  12928  cospi  12929  efipi  12930  eulerid  12931  sin2pi  12932  cos2pi  12933  ef2pi  12934  sincosq4sgn  12958  cosq14gt0  12961  tangtx  12967  sincos4thpi  12969  sincos6thpi  12971  sinkpi  12976  cosq34lt1  12979  dfrelog  12989  2logb9irr  13096  2logb9irrALT  13099  2logb9irrap  13102  ex-fl  13108  ex-exp  13110  ex-fac  13111  ex-bc  13112  ex-dvds  13113  ex-gcd  13114  bj-dfom  13302  012of  13363  2o01f  13364  pwle2  13366  exmid1stab  13368  nninfsellemqall  13386  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419  dceqnconst  13423  taupi  13430