Theorem eqtri 2186

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqtr2i  2187  eqtr3i  2188  eqtr4i  2189  3eqtri  2190  3eqtrri  2191  3eqtr2i  2192  cbvrab  2723  csb2  3046  cbvrabcsf  3109  difjust  3116  unjust  3118  injust  3120  dfdif3  3231  difeq12i  3237  inrot  3336  symdif1  3386  rabnc  3440  0in  3443  ssdifin0  3489  dfif3  3532  ifbieq2i  3542  ifbieq12i  3544  pwjust  3559  snjust  3580  dfpr2  3594  disjpr2  3639  difprsn1  3711  diftpsn3  3713  difpr  3714  dfuni2  3790  intab  3852  intunsn  3861  rint0  3862  iunid  3920  viin  3924  iinrabm  3927  2iunin  3931  riin0  3936  iunxprg  3945  unopab  4060  cbvmptf  4075  cbvmpt  4076  unisucg  4391  op1stb  4455  orddif  4523  elxpi  4619  csbxpg  4684  relopabi  4729  inxp  4737  coeq12i  4766  dfdm3  4790  dfrn3  4792  dmun  4810  dmopab  4814  dmopab3  4816  dmxpid  4824  dmxpin  4825  rnopab  4850  rnmpt  4851  rncoss  4873  rncoeq  4876  reseq12i  4881  resundi  4896  resindi  4898  resiun1  4902  resdmdfsn  4926  resopab  4927  mptresid  4937  dfima3  4948  imadisj  4965  ndmima  4980  mptcnv  5005  rnun  5011  rnuni  5014  imaundi  5015  inimass  5019  cnvxp  5021  rnxpm  5032  dminxp  5047  imainrect  5048  cnvcnv3  5052  dmpropg  5075  op1sta  5084  op2ndb  5086  op2nda  5087  resdmres  5094  mptpreima  5096  coundi  5104  coundir  5105  cocnvcnv1  5113  cores2  5115  dfdm2  5137  iotajust  5151  dfiota2  5153  funi  5219  funtp  5240  fntpg  5243  funcnvuni  5256  funcnvres  5260  imadiflem  5266  imadif  5267  imainlem  5268  imain  5269  fnresdisj  5297  mptfng  5312  resdif  5453  fv2  5480  dffv4g  5482  fveq12i  5491  nfvres  5518  0fv  5520  dfimafn2  5535  fnimapr  5545  fvmptss2  5560  fvmptg  5561  fvmpts  5563  fvmpt2  5568  mptfvex  5570  elfvmptrab  5580  fvopab6  5581  f1ompt  5635  dfmpt  5661  ressnop0  5665  fprg  5667  fvsnun1  5681  fsnunfv  5685  fvpr2g  5691  imauni  5728  fliftfuns  5765  cbvriota  5807  oveq123i  5855  fconstmpo  5933  resoprab  5934  mpofun  5940  rnmpo  5948  reldmmpo  5949  ov  5957  ovigg  5958  ovmpt4g  5960  ovg  5976  caov31  6027  elmpocl  6035  f1ocnvd  6039  oprabrexex2  6095  op1st  6111  op2nd  6112  f1stres  6124  f2ndres  6125  unielxp  6139  dfoprab3s  6155  dfoprab4  6157  mpompts  6163  mpofvex  6168  oprab2co  6182  df1st2  6183  df2nd2  6184  f1od2  6199  brtpos0  6216  tposoprab  6244  smores3  6257  tfrlemi14d  6297  tfr1onlemaccex  6312  tfrcllemaccex  6325  rdgisuc1  6348  rdg0  6351  frec0g  6361  df1o2  6393  df2o2  6395  oasuc  6428  omv2  6429  omsuc  6436  ecidsn  6544  qliftfuns  6581  oviec  6603  mapsncnv  6657  dfixp  6662  xpcomco  6788  xpassen  6792  ssenen  6813  undifdc  6885  unfiin  6887  fidcenumlemrks  6914  fidcenumlemr  6916  sbthlemi5  6922  sbthlemi8  6925  fi0  6936  inf00  6992  djuf1olemr  7015  djuinr  7024  djuin  7025  djuun  7028  casefun  7046  casedm  7047  caseinj  7050  caseinl  7052  caseinr  7053  endjusym  7057  eninl  7058  eninr  7059  djudm  7066  djuinj  7067  fodjuomni  7109  fodjumkv  7120  pm54.43  7142  exmidfodomrlemim  7153  xp2dju  7167  djucomen  7168  djuassen  7169  xpdjuen  7170  pw1nel3  7183  sucpw1nel3  7185  addpiord  7253  mulpiord  7254  dmaddpi  7262  dmmulpi  7263  recmulnqg  7328  1lt2nq  7343  halfnqq  7347  dfmq0qs  7366  dfplq0qs  7367  genpdf  7445  1prl  7492  1pru  7493  ltexprlemell  7535  ltexprlemelu  7536  recexprlemell  7559  recexprlemelu  7560  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdrl  7594  cauappcvgprlem2  7597  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem2  7617  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemclphr  7642  caucvgprprlemexbt  7643  caucvgprprlem2  7647  addsrpr  7682  mulsrpr  7683  caucvgsrlemoffres  7737  caucvgsr  7739  suplocsrlempr  7744  addcnsr  7771  mulcnsr  7772  mulresr  7775  addvalex  7781  pitonnlem1  7782  axi2m1  7812  axcnre  7818  mulcomli  7902  mnfnre  7937  addcomli  8039  add42i  8060  mvrraddi  8111  neg0  8140  negdii  8178  negsubdi2i  8180  crap0  8849  2t2e4  9007  3t2e6  9009  3t3e9  9010  4t2e8  9011  neg1mulneg1e1  9065  8th4div3  9072  halfpm6th  9073  iap0  9076  dfdec10  9321  deceq12i  9326  numltc  9343  decsuc  9348  decsucc  9358  nummac  9362  numma2c  9363  numadd  9364  numaddc  9365  nummul1c  9366  nummul2c  9367  decma  9368  decmac  9369  decma2c  9370  decadd  9371  decaddc  9372  decrmanc  9374  decrmac  9375  decaddci  9378  decsubi  9380  decmul1  9381  decmul1c  9382  decmul2c  9383  11multnc  9385  4t3lem  9414  6t2e12  9421  7t2e14  9426  8t2e16  9432  9t2e18  9439  9t11e99  9447  halfthird  9460  5recm6rec  9461  divfnzn  9555  xnegpnf  9760  xneg0  9763  xaddmnf1  9780  xaddmnf2  9781  mnfaddpnf  9783  iooval2  9847  dfioo2  9906  fzval2  9943  fzsuc2  10010  fztpval  10014  fz0to3un2pr  10054  fz0to4untppr  10055  fzo01  10147  fzo12sn  10148  fzo0to42pr  10151  fldiv4p1lem1div2  10236  intqfrac2  10250  intfracq  10251  1tonninf  10371  neg1sqe1  10545  sq2  10546  sq3  10547  cu2  10549  i2  10551  i3  10552  binom2i  10559  sq10  10621  3dec  10623  facp1  10639  fac2  10640  fac4  10642  4bc2eq6  10683  hashp1i  10719  pr0hash2ex  10724  hashfzo  10731  hashxp  10735  zfz1isolem1  10749  cji  10840  cnrecnv  10848  sqrt0  10942  resqrexlemover  10948  resqrexlemcalc3  10954  absi  10997  absimle  11022  sumeq12i  11302  summodclem2a  11318  summodc  11320  sum0  11325  fsumsplitf  11345  fsum2dlemstep  11371  fsumabs  11402  fsumiun  11414  0.999...  11458  mertenslem2  11473  prodeq12i  11500  prodmodc  11515  fprod2dlemstep  11559  ege2le3  11608  eft0val  11630  cos0  11667  cos1bnd  11696  cos2bnd  11697  3dvdsdec  11798  3dvds2dec  11799  odd2np1  11806  opoe  11828  nn0o  11840  gcd0val  11889  6gcd4e2  11924  nnmindc  11963  nnminle  11964  3lcm2e6woprm  12014  3lcm2e6  12088  nn0gcdsq  12128  phiprmpw  12150  phimullem  12153  pcprecl  12217  pcprendvds  12218  pcmptdvds  12271  pockthi  12284  unennn  12326  ennnfonelemj0  12330  ennnfonelem0  12334  ennnfonelem1  12336  ennnfonelemhf1o  12342  ennnfonelemrn  12348  ennnfonelemdm  12349  strnfvnd  12410  slotslfn  12416  setsfun  12425  setsfun0  12426  setscom  12430  setsslid  12440  2strstr1g  12493  cnco  12821  txuni2  12856  txbas  12858  uptx  12874  txcn  12875  cnmptid  12881  cnmpt2t  12893  xmetxp  13107  cnmetdval  13129  remetdval  13139  resubmet  13148  rerestcntop  13150  divcnap  13155  cnrehmeocntop  13193  dvexp  13275  sinhalfpilem  13312  cosneghalfpi  13319  efhalfpi  13320  cospi  13321  efipi  13322  eulerid  13323  sin2pi  13324  cos2pi  13325  ef2pi  13326  sincosq4sgn  13350  cosq14gt0  13353  tangtx  13359  sincos4thpi  13361  sincos6thpi  13363  sinkpi  13368  cosq34lt1  13371  dfrelog  13381  2logb9irr  13489  2logb9irrALT  13492  2logb9irrap  13495  zabsle1  13500  lgslem2  13502  lgsfcl2  13507  lgsdir2lem1  13529  lgsdir2lem2  13530  lgsdir2lem4  13532  lgsdir2lem5  13533  ex-fl  13566  ex-exp  13568  ex-fac  13569  ex-bc  13570  ex-dvds  13571  ex-gcd  13572  bj-dfom  13775  012of  13835  2o01f  13836  pwle2  13838  exmid1stab  13840  nninfsellemqall  13855  isomninnlem  13869  iswomninnlem  13888  ismkvnnlem  13891  dceqnconst  13898  dcapnconst  13899  taupi  13909