Theorem eqtri 2198

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

Syntax hints:   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqtr2i  2199  eqtr3i  2200  eqtr4i  2201  3eqtri  2202  3eqtrri  2203  3eqtr2i  2204  cbvrab  2735  csb2  3059  cbvrabcsf  3122  difjust  3130  unjust  3132  injust  3134  dfdif3  3245  difeq12i  3251  inrot  3350  symdif1  3400  rabnc  3455  0in  3458  ssdifin0  3504  dfif3  3547  ifbieq2i  3557  ifbieq12i  3559  pwjust  3575  snjust  3596  dfpr2  3610  disjpr2  3655  difprsn1  3730  diftpsn3  3732  difpr  3733  dfuni2  3809  intab  3871  intunsn  3880  rint0  3881  iunid  3939  viin  3943  iinrabm  3946  2iunin  3950  riin0  3955  iunxprg  3964  unopab  4079  cbvmptf  4094  cbvmpt  4095  exmid1stab  4205  unisucg  4411  op1stb  4475  orddif  4543  elxpi  4639  csbxpg  4704  relopabi  4749  inxp  4757  coeq12i  4786  dfdm3  4810  dfrn3  4812  dmun  4830  dmopab  4834  dmopab3  4836  dmxpid  4844  dmxpin  4845  rnopab  4870  rnmpt  4871  rncoss  4893  rncoeq  4896  reseq12i  4901  resundi  4916  resindi  4918  resiun1  4922  resdmdfsn  4946  resopab  4947  mptresid  4957  dfima3  4969  imadisj  4986  ndmima  5001  mptcnv  5027  rnun  5033  rnuni  5036  imaundi  5037  inimass  5041  cnvxp  5043  rnxpm  5054  dminxp  5069  imainrect  5070  cnvcnv3  5074  dmpropg  5097  op1sta  5106  op2ndb  5108  op2nda  5109  resdmres  5116  mptpreima  5118  coundi  5126  coundir  5127  cocnvcnv1  5135  cores2  5137  dfdm2  5159  iotajust  5173  dfiota2  5175  funi  5244  funtp  5265  fntpg  5268  funcnvuni  5281  funcnvres  5285  imadiflem  5291  imadif  5292  imainlem  5293  imain  5294  fnresdisj  5322  mptfng  5337  resdif  5479  fv2  5506  dffv4g  5508  fveq12i  5517  nfvres  5544  0fv  5546  dfimafn2  5561  fnimapr  5572  fvmptss2  5587  fvmptg  5588  fvmpts  5590  fvmpt2  5595  mptfvex  5597  elfvmptrab  5607  fvopab6  5608  f1ompt  5663  dfmpt  5689  ressnop0  5693  fprg  5695  fvsnun1  5709  fsnunfv  5713  fvpr2g  5719  imauni  5756  fliftfuns  5793  cbvriota  5835  oveq123i  5883  fconstmpo  5964  resoprab  5965  mpofun  5971  rnmpo  5979  reldmmpo  5980  ov  5988  ovigg  5989  ovmpt4g  5991  ovg  6007  caov31  6058  elmpocl  6063  f1ocnvd  6067  oprabrexex2  6125  op1st  6141  op2nd  6142  f1stres  6154  f2ndres  6155  unielxp  6169  dfoprab3s  6185  dfoprab4  6187  mpompts  6193  mpofvex  6198  oprab2co  6213  df1st2  6214  df2nd2  6215  f1od2  6230  brtpos0  6247  tposoprab  6275  smores3  6288  tfrlemi14d  6328  tfr1onlemaccex  6343  tfrcllemaccex  6356  rdgisuc1  6379  rdg0  6382  frec0g  6392  df1o2  6424  df2o2  6426  oasuc  6459  omv2  6460  omsuc  6467  ecidsn  6576  qliftfuns  6613  oviec  6635  mapsncnv  6689  dfixp  6694  xpcomco  6820  xpassen  6824  ssenen  6845  undifdc  6917  unfiin  6919  fidcenumlemrks  6946  fidcenumlemr  6948  sbthlemi5  6954  sbthlemi8  6957  fi0  6968  inf00  7024  djuf1olemr  7047  djuinr  7056  djuin  7057  djuun  7060  casefun  7078  casedm  7079  caseinj  7082  caseinl  7084  caseinr  7085  endjusym  7089  eninl  7090  eninr  7091  djudm  7098  djuinj  7099  fodjuomni  7141  fodjumkv  7152  nninfwlporlemd  7164  pm54.43  7183  exmidfodomrlemim  7194  xp2dju  7208  djucomen  7209  djuassen  7210  xpdjuen  7211  pw1nel3  7224  sucpw1nel3  7226  addpiord  7303  mulpiord  7304  dmaddpi  7312  dmmulpi  7313  recmulnqg  7378  1lt2nq  7393  halfnqq  7397  dfmq0qs  7416  dfplq0qs  7417  genpdf  7495  1prl  7542  1pru  7543  ltexprlemell  7585  ltexprlemelu  7586  recexprlemell  7609  recexprlemelu  7610  cauappcvgprlemm  7632  cauappcvgprlemopl  7633  cauappcvgprlemlol  7634  cauappcvgprlemopu  7635  cauappcvgprlemupu  7636  cauappcvgprlemdisj  7638  cauappcvgprlemloc  7639  cauappcvgprlemladdfu  7641  cauappcvgprlemladdfl  7642  cauappcvgprlemladdrl  7644  cauappcvgprlem2  7647  caucvgprlemm  7655  caucvgprlemopl  7656  caucvgprlemlol  7657  caucvgprlemopu  7658  caucvgprlemupu  7659  caucvgprlemdisj  7661  caucvgprlemloc  7662  caucvgprlemcl  7663  caucvgprlemladdfu  7664  caucvgprlemladdrl  7665  caucvgprlem2  7667  caucvgprprlemell  7672  caucvgprprlemelu  7673  caucvgprprlemml  7681  caucvgprprlemmu  7682  caucvgprprlemclphr  7692  caucvgprprlemexbt  7693  caucvgprprlem2  7697  addsrpr  7732  mulsrpr  7733  caucvgsrlemoffres  7787  caucvgsr  7789  suplocsrlempr  7794  addcnsr  7821  mulcnsr  7822  mulresr  7825  addvalex  7831  pitonnlem1  7832  axi2m1  7862  axcnre  7868  mulcomli  7952  mnfnre  7987  addcomli  8089  add42i  8110  mvrraddi  8161  neg0  8190  negdii  8228  negsubdi2i  8230  crap0  8901  2t2e4  9059  3t2e6  9061  3t3e9  9062  4t2e8  9063  neg1mulneg1e1  9117  8th4div3  9124  halfpm6th  9125  iap0  9128  dfdec10  9373  deceq12i  9378  numltc  9395  decsuc  9400  decsucc  9410  nummac  9414  numma2c  9415  numadd  9416  numaddc  9417  nummul1c  9418  nummul2c  9419  decma  9420  decmac  9421  decma2c  9422  decadd  9423  decaddc  9424  decrmanc  9426  decrmac  9427  decaddci  9430  decsubi  9432  decmul1  9433  decmul1c  9434  decmul2c  9435  11multnc  9437  4t3lem  9466  6t2e12  9473  7t2e14  9478  8t2e16  9484  9t2e18  9491  9t11e99  9499  halfthird  9512  5recm6rec  9513  divfnzn  9607  xnegpnf  9812  xneg0  9815  xaddmnf1  9832  xaddmnf2  9833  mnfaddpnf  9835  iooval2  9899  dfioo2  9958  fzval2  9995  fzsuc2  10062  fztpval  10066  fz0to3un2pr  10106  fz0to4untppr  10107  fzo01  10199  fzo12sn  10200  fzo0to42pr  10203  fldiv4p1lem1div2  10288  intqfrac2  10302  intfracq  10303  1tonninf  10423  neg1sqe1  10597  sq2  10598  sq3  10599  cu2  10601  i2  10603  i3  10604  binom2i  10611  sq10  10673  3dec  10675  facp1  10691  fac2  10692  fac4  10694  4bc2eq6  10735  hashp1i  10771  pr0hash2ex  10776  hashfzo  10783  hashxp  10787  zfz1isolem1  10801  cji  10892  cnrecnv  10900  sqrt0  10994  resqrexlemover  11000  resqrexlemcalc3  11006  absi  11049  absimle  11074  sumeq12i  11354  summodclem2a  11370  summodc  11372  sum0  11377  fsumsplitf  11397  fsum2dlemstep  11423  fsumabs  11454  fsumiun  11466  0.999...  11510  mertenslem2  11525  prodeq12i  11552  prodmodc  11567  fprod2dlemstep  11611  ege2le3  11660  eft0val  11682  cos0  11719  cos1bnd  11748  cos2bnd  11749  3dvdsdec  11850  3dvds2dec  11851  odd2np1  11858  opoe  11880  nn0o  11892  gcd0val  11941  6gcd4e2  11976  nnmindc  12015  nnminle  12016  3lcm2e6woprm  12066  3lcm2e6  12140  nn0gcdsq  12180  phiprmpw  12202  phimullem  12205  pcprecl  12269  pcprendvds  12270  pcmptdvds  12323  pockthi  12336  unennn  12378  ennnfonelemj0  12382  ennnfonelem0  12386  ennnfonelem1  12388  ennnfonelemhf1o  12394  ennnfonelemrn  12400  ennnfonelemdm  12401  strnfvnd  12462  slotslfn  12468  setsfun  12477  setsfun0  12478  setscom  12482  setsslid  12492  2strstr1g  12556  cnco  13381  txuni2  13416  txbas  13418  uptx  13434  txcn  13435  cnmptid  13441  cnmpt2t  13453  xmetxp  13667  cnmetdval  13689  remetdval  13699  resubmet  13708  rerestcntop  13710  divcnap  13715  cnrehmeocntop  13753  dvexp  13835  sinhalfpilem  13872  cosneghalfpi  13879  efhalfpi  13880  cospi  13881  efipi  13882  eulerid  13883  sin2pi  13884  cos2pi  13885  ef2pi  13886  sincosq4sgn  13910  cosq14gt0  13913  tangtx  13919  sincos4thpi  13921  sincos6thpi  13923  sinkpi  13928  cosq34lt1  13931  dfrelog  13941  2logb9irr  14049  2logb9irrALT  14052  2logb9irrap  14055  zabsle1  14060  lgslem2  14062  lgsfcl2  14067  lgsdir2lem1  14089  lgsdir2lem2  14090  lgsdir2lem4  14092  lgsdir2lem5  14093  ex-fl  14126  ex-exp  14128  ex-fac  14129  ex-bc  14130  ex-dvds  14131  ex-gcd  14132  bj-dfom  14334  012of  14394  2o01f  14395  pwle2  14397  nninfsellemqall  14413  isomninnlem  14427  iswomninnlem  14446  ismkvnnlem  14449  dceqnconst  14456  dcapnconst  14457  taupi  14467