Theorem eqtri 2160

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

Syntax hints:   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  eqtr2i  2161  eqtr3i  2162  eqtr4i  2163  3eqtri  2164  3eqtrri  2165  3eqtr2i  2166  cbvrab  2684  csb2  3005  cbvrabcsf  3065  difjust  3072  unjust  3074  injust  3076  dfdif3  3186  difeq12i  3192  inrot  3291  symdif1  3341  rabnc  3395  0in  3398  ssdifin0  3444  dfif3  3487  ifbieq2i  3495  ifbieq12i  3497  pwjust  3511  snjust  3532  dfpr2  3546  disjpr2  3587  difprsn1  3659  diftpsn3  3661  difpr  3662  dfuni2  3738  intab  3800  intunsn  3809  rint0  3810  iunid  3868  viin  3872  iinrabm  3875  2iunin  3879  riin0  3884  iunxprg  3893  unopab  4007  cbvmptf  4022  cbvmpt  4023  unisucg  4336  op1stb  4399  orddif  4462  elxpi  4555  csbxpg  4620  relopabi  4665  inxp  4673  coeq12i  4702  dfdm3  4726  dfrn3  4728  dmun  4746  dmopab  4750  dmopab3  4752  dmxpid  4760  dmxpin  4761  rnopab  4786  rnmpt  4787  rncoss  4809  rncoeq  4812  reseq12i  4817  resundi  4832  resindi  4834  resiun1  4838  resdmdfsn  4862  resopab  4863  mptresid  4873  dfima3  4884  imadisj  4901  ndmima  4916  mptcnv  4941  rnun  4947  rnuni  4950  imaundi  4951  inimass  4955  cnvxp  4957  rnxpm  4968  dminxp  4983  imainrect  4984  cnvcnv3  4988  dmpropg  5011  op1sta  5020  op2ndb  5022  op2nda  5023  resdmres  5030  mptpreima  5032  coundi  5040  coundir  5041  cocnvcnv1  5049  cores2  5051  dfdm2  5073  iotajust  5087  dfiota2  5089  funi  5155  funtp  5176  fntpg  5179  funcnvuni  5192  funcnvres  5196  imadiflem  5202  imadif  5203  imainlem  5204  imain  5205  fnresdisj  5233  mptfng  5248  resdif  5389  fv2  5416  dffv4g  5418  fveq12i  5427  nfvres  5454  0fv  5456  dfimafn2  5471  fnimapr  5481  fvmptss2  5496  fvmptg  5497  fvmpts  5499  fvmpt2  5504  mptfvex  5506  elfvmptrab  5516  fvopab6  5517  f1ompt  5571  dfmpt  5597  ressnop0  5601  fprg  5603  fvsnun1  5617  fsnunfv  5621  fvpr2g  5627  imauni  5662  fliftfuns  5699  cbvriota  5740  oveq123i  5788  fconstmpo  5866  resoprab  5867  mpofun  5873  rnmpo  5881  reldmmpo  5882  ov  5890  ovigg  5891  ovmpt4g  5893  ovg  5909  caov31  5960  elmpocl  5968  f1ocnvd  5972  oprabrexex2  6028  op1st  6044  op2nd  6045  f1stres  6057  f2ndres  6058  unielxp  6072  dfoprab3s  6088  dfoprab4  6090  mpompts  6096  mpofvex  6101  oprab2co  6115  df1st2  6116  df2nd2  6117  f1od2  6132  brtpos0  6149  tposoprab  6177  smores3  6190  tfrlemi14d  6230  tfr1onlemaccex  6245  tfrcllemaccex  6258  rdgisuc1  6281  rdg0  6284  frec0g  6294  df1o2  6326  df2o2  6328  oasuc  6360  omv2  6361  omsuc  6368  ecidsn  6476  qliftfuns  6513  oviec  6535  mapsncnv  6589  dfixp  6594  xpcomco  6720  xpassen  6724  ssenen  6745  undifdc  6812  unfiin  6814  fidcenumlemrks  6841  fidcenumlemr  6843  sbthlemi5  6849  sbthlemi8  6852  fi0  6863  inf00  6918  djuf1olemr  6939  djuinr  6948  djuin  6949  djuun  6952  casefun  6970  casedm  6971  caseinj  6974  caseinl  6976  caseinr  6977  endjusym  6981  eninl  6982  eninr  6983  djudm  6990  djuinj  6991  fodjuomni  7021  fodjumkv  7034  pm54.43  7046  exmidfodomrlemim  7057  xp2dju  7071  djucomen  7072  djuassen  7073  xpdjuen  7074  addpiord  7124  mulpiord  7125  dmaddpi  7133  dmmulpi  7134  recmulnqg  7199  1lt2nq  7214  halfnqq  7218  dfmq0qs  7237  dfplq0qs  7238  genpdf  7316  1prl  7363  1pru  7364  ltexprlemell  7406  ltexprlemelu  7407  recexprlemell  7430  recexprlemelu  7431  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemupu  7457  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdrl  7465  cauappcvgprlem2  7468  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemupu  7480  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem2  7488  caucvgprprlemell  7493  caucvgprprlemelu  7494  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemclphr  7513  caucvgprprlemexbt  7514  caucvgprprlem2  7518  addsrpr  7553  mulsrpr  7554  caucvgsrlemoffres  7608  caucvgsr  7610  suplocsrlempr  7615  addcnsr  7642  mulcnsr  7643  mulresr  7646  addvalex  7652  pitonnlem1  7653  axi2m1  7683  axcnre  7689  mulcomli  7773  mnfnre  7808  addcomli  7907  add42i  7928  mvrraddi  7979  neg0  8008  negdii  8046  negsubdi2i  8048  crap0  8716  2t2e4  8874  3t2e6  8876  3t3e9  8877  4t2e8  8878  neg1mulneg1e1  8932  8th4div3  8939  halfpm6th  8940  iap0  8943  dfdec10  9185  deceq12i  9190  numltc  9207  decsuc  9212  decsucc  9222  nummac  9226  numma2c  9227  numadd  9228  numaddc  9229  nummul1c  9230  nummul2c  9231  decma  9232  decmac  9233  decma2c  9234  decadd  9235  decaddc  9236  decrmanc  9238  decrmac  9239  decaddci  9242  decsubi  9244  decmul1  9245  decmul1c  9246  decmul2c  9247  11multnc  9249  4t3lem  9278  6t2e12  9285  7t2e14  9290  8t2e16  9296  9t2e18  9303  9t11e99  9311  halfthird  9324  5recm6rec  9325  divfnzn  9413  xnegpnf  9611  xneg0  9614  xaddmnf1  9631  xaddmnf2  9632  mnfaddpnf  9634  iooval2  9698  dfioo2  9757  fzval2  9793  fzsuc2  9859  fztpval  9863  fzo01  9993  fzo12sn  9994  fzo0to42pr  9997  fldiv4p1lem1div2  10078  intqfrac2  10092  intfracq  10093  1tonninf  10213  neg1sqe1  10387  sq2  10388  sq3  10389  cu2  10391  i2  10393  i3  10394  binom2i  10401  sq10  10459  3dec  10461  facp1  10476  fac2  10477  fac4  10479  4bc2eq6  10520  hashp1i  10556  pr0hash2ex  10561  hashfzo  10568  hashxp  10572  zfz1isolem1  10583  cji  10674  cnrecnv  10682  sqrt0  10776  resqrexlemover  10782  resqrexlemcalc3  10788  absi  10831  absimle  10856  sumeq12i  11134  summodclem2a  11150  summodc  11152  sum0  11157  fsumsplitf  11177  fsum2dlemstep  11203  fsumabs  11234  fsumiun  11246  0.999...  11290  mertenslem2  11305  prodeq12i  11332  prodmodc  11347  ege2le3  11377  eft0val  11399  cos0  11437  cos1bnd  11466  cos2bnd  11467  3dvdsdec  11562  3dvds2dec  11563  odd2np1  11570  opoe  11592  nn0o  11604  gcd0val  11649  6gcd4e2  11683  3lcm2e6woprm  11767  3lcm2e6  11838  nn0gcdsq  11878  phiprmpw  11898  phimullem  11901  unennn  11910  ennnfonelemj0  11914  ennnfonelem0  11918  ennnfonelem1  11920  ennnfonelemhf1o  11926  ennnfonelemrn  11932  ennnfonelemdm  11933  strnfvnd  11979  slotslfn  11985  setsfun  11994  setsfun0  11995  setscom  11999  setsslid  12009  2strstr1g  12062  cnco  12390  txuni2  12425  txbas  12427  uptx  12443  txcn  12444  cnmptid  12450  cnmpt2t  12462  xmetxp  12676  cnmetdval  12698  remetdval  12708  resubmet  12717  rerestcntop  12719  divcnap  12724  cnrehmeocntop  12762  dvexp  12844  sinhalfpilem  12872  cosneghalfpi  12879  efhalfpi  12880  cospi  12881  efipi  12882  eulerid  12883  sin2pi  12884  cos2pi  12885  ef2pi  12886  sincosq4sgn  12910  cosq14gt0  12913  tangtx  12919  sincos4thpi  12921  sincos6thpi  12923  sinkpi  12928  cosq34lt1  12931  ex-fl  12937  ex-exp  12939  ex-fac  12940  ex-bc  12941  ex-dvds  12942  ex-gcd  12943  bj-dfom  13131  pwle2  13193  exmid1stab  13195  nninfsellemqall  13211  isomninnlem  13225  taupi  13239