Theorem eqtri 2101

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

Syntax hints:   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  eqtr2i  2102  eqtr3i  2103  eqtr4i  2104  3eqtri  2105  3eqtrri  2106  3eqtr2i  2107  cbvrab  2599  csb2  2910  cbvrabcsf  2967  difjust  2974  unjust  2976  injust  2978  difeq12i  3088  inrot  3181  symdif1  3229  rabnc  3277  ssdifin0  3324  dfif3  3364  ifbieq2i  3372  ifbieq12i  3374  pwjust  3383  snjust  3403  dfpr2  3417  disjpr2  3456  difprsn1  3525  diftpsn3  3527  dfuni2  3603  intab  3665  intunsn  3674  rint0  3675  iunid  3733  viin  3737  iinrabm  3740  2iunin  3744  riin0  3749  unopab  3857  cbvmpt  3872  unisucg  4169  op1stb  4227  orddif  4290  elxpi  4379  csbxpg  4439  relopabi  4481  inxp  4488  coeq12i  4517  dfdm3  4540  dfrn3  4542  dmun  4560  dmopab  4564  dmopab3  4566  rnopab  4599  rnmpt  4600  rncoss  4620  rncoeq  4623  reseq12i  4628  resundi  4643  resindi  4645  resiun1  4648  resdmdfsn  4671  resopab  4672  mptresid  4680  dfima3  4691  imadisj  4707  ndmima  4722  rnun  4752  rnuni  4755  imaundi  4756  inimass  4760  cnvxp  4762  rnxpm  4772  dminxp  4785  imainrect  4786  cnvcnv3  4790  dmpropg  4813  op1sta  4822  op2ndb  4824  op2nda  4825  resdmres  4832  mptpreima  4834  coundi  4842  coundir  4843  cocnvcnv1  4851  cores2  4853  dfdm2  4872  iotajust  4886  dfiota2  4888  funi  4952  funtp  4972  fntpg  4975  funcnvuni  4988  funcnvres  4992  imadiflem  4998  imadif  4999  imainlem  5000  imain  5001  fnresdisj  5029  mptfng  5044  resdif  5168  fv2  5193  dffv4g  5195  fveq12i  5203  nfvres  5227  0fv  5229  dfimafn2  5244  fnimapr  5254  fvmptss2  5268  fvmptg  5269  fvmpts  5271  fvmpt2  5275  mptfvex  5277  fvopab6  5285  f1ompt  5341  dfmpt  5361  ressnop0  5365  fprg  5367  fvsnun1  5381  fsnunfv  5384  fvpr2g  5389  imauni  5421  fliftfuns  5458  cbvriota  5498  oveq123i  5546  resoprab  5617  mpt2fun  5623  rnmpt2  5631  reldmmpt2  5632  ov  5640  ovigg  5641  ovmpt4g  5643  ovg  5659  caov31  5710  elmpt2cl  5718  f1ocnvd  5722  oprabrexex2  5777  op1st  5793  op2nd  5794  f1stres  5806  f2ndres  5807  unielxp  5820  dfoprab3s  5836  dfoprab4  5838  mpt2mpts  5844  mpt2fvex  5849  oprab2co  5859  df1st2  5860  df2nd2  5861  f1od2  5876  brtpos0  5890  tposoprab  5918  smores3  5931  tfrlemi14d  5970  rdgisuc1  5994  rdg0  5997  frec0g  6006  frecsuc  6014  df1o2  6036  df2o2  6038  oasuc  6067  omv2  6068  omsuc  6074  ecidsn  6176  qliftfuns  6213  oviec  6235  xpcomco  6323  xpassen  6327  inf00  6444  pm54.43  6459  addpiord  6506  mulpiord  6507  dmaddpi  6515  dmmulpi  6516  recmulnqg  6581  1lt2nq  6596  halfnqq  6600  dfmq0qs  6619  dfplq0qs  6620  genpdf  6698  1prl  6745  1pru  6746  ltexprlemell  6788  ltexprlemelu  6789  recexprlemell  6812  recexprlemelu  6813  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemupu  6839  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdrl  6847  cauappcvgprlem2  6850  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemupu  6862  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem2  6870  caucvgprprlemell  6875  caucvgprprlemelu  6876  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemclphr  6895  caucvgprprlemexbt  6896  caucvgprprlem2  6900  addsrpr  6922  mulsrpr  6923  caucvgsrlemoffres  6976  caucvgsr  6978  addcnsr  7002  mulcnsr  7003  mulresr  7006  addvalex  7012  pitonnlem1  7013  axi2m1  7041  axcnre  7047  mulcomli  7126  mnfnre  7161  addcomli  7253  add42i  7274  mvrraddi  7325  neg0  7354  negdii  7392  negsubdi2i  7394  crap0  8035  2t2e4  8186  3t2e6  8188  3t3e9  8189  4t2e8  8190  neg1mulneg1e1  8243  8th4div3  8250  halfpm6th  8251  iap0  8254  dfdec10  8480  deceq12i  8485  numltc  8502  decsuc  8507  decsucc  8517  nummac  8521  numma2c  8522  numadd  8523  numaddc  8524  nummul1c  8525  nummul2c  8526  decma  8527  decmac  8528  decma2c  8529  decadd  8530  decaddc  8531  decrmanc  8533  decrmac  8534  decaddci  8537  decsubi  8539  decmul1  8540  decmul1c  8541  decmul2c  8542  11multnc  8544  4t3lem  8573  6t2e12  8580  7t2e14  8585  8t2e16  8591  9t2e18  8598  9t11e99  8606  divfnzn  8706  xnegpnf  8895  xneg0  8898  iooval2  8938  dfioo2  8997  fzval2  9032  fzsuc2  9096  fztpval  9100  fzo01  9225  fzo12sn  9226  fzo0to42pr  9229  fldiv4p1lem1div2  9307  intqfrac2  9321  intfracq  9322  neg1sqe1  9570  sq2  9571  sq3  9572  cu2  9573  i2  9575  i3  9576  binom2i  9583  sq10  9640  3dec  9642  facp1  9657  fac2  9658  fac4  9660  4bc2eq6  9701  cji  9789  cnrecnv  9797  sqrt0  9890  resqrexlemover  9896  resqrexlemcalc3  9902  absi  9945  absimle  9970  3dvdsdec  10264  3dvds2dec  10265  odd2np1  10272  opoe  10295  nn0o  10307  gcd0val  10352  6gcd4e2  10384  3lcm2e6woprm  10468  3lcm2e6  10539  ex-fl  10563  ex-fac  10565  ex-bc  10566  ex-dvds  10567  ex-gcd  10568  bj-dfom  10728