Theorem eqtri 2214

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtri.1	⊢ 𝐴 = 𝐵
eqtri.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eqtri	⊢ 𝐴 = 𝐶

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	eqeq2i 2204	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐴 = 𝐶)
4	1, 3	mpbi 145	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtr2i  2215  eqtr3i  2216  eqtr4i  2217  3eqtri  2218  3eqtrri  2219  3eqtr2i  2220  cbvrab  2758  csb2  3083  cbvrabcsf  3147  difjust  3155  unjust  3157  injust  3159  dfdif3  3270  difeq12i  3276  inrot  3375  symdif1  3425  rabnc  3480  0in  3483  ssdifin0  3529  dfif3  3571  ifbieq2i  3581  ifbieq12i  3583  pwjust  3603  snjust  3624  dfpr2  3638  disjpr2  3683  difprsn1  3758  diftpsn3  3760  difpr  3761  dfuni2  3838  intab  3900  intunsn  3909  rint0  3910  iunid  3969  viin  3973  iinrabm  3976  2iunin  3980  riin0  3985  iunxprg  3994  unopab  4109  cbvmptf  4124  cbvmpt  4125  exmid1stab  4238  unisucg  4446  op1stb  4510  orddif  4580  elxpi  4676  csbxpg  4741  relopabi  4788  inxp  4797  coeq12i  4826  dfdm3  4850  dfrn3  4852  dmun  4870  dmopab  4874  dmopab3  4876  dmxpid  4884  dmxpin  4885  rnopab  4910  rnmpt  4911  rncoss  4933  rncoeq  4936  reseq12i  4941  resundi  4956  resindi  4958  resiun1  4962  resdmdfsn  4986  resopab  4987  opabresid  4996  dfima3  5009  mptima  5018  imadisj  5028  ndmima  5043  mptcnv  5069  rnun  5075  rnuni  5078  imaundi  5079  inimass  5083  cnvxp  5085  rnxpm  5096  dminxp  5111  imainrect  5112  cnvcnv3  5116  dmpropg  5139  op1sta  5148  op2ndb  5150  op2nda  5151  resdmres  5158  mptpreima  5160  coundi  5168  coundir  5169  cocnvcnv1  5177  cores2  5179  dfdm2  5201  iotajust  5215  dfiota2  5217  funi  5287  funtp  5308  fntpg  5311  funcnvuni  5324  funcnvres  5328  imadiflem  5334  imadif  5335  imainlem  5336  imain  5337  fnresdisj  5365  mptfng  5380  resdif  5523  fv2  5550  dffv4g  5552  fveq12i  5561  nfvres  5589  0fv  5591  dfimafn2  5607  fnimapr  5618  fvmptss2  5633  fvmptg  5634  fvmpts  5636  fvmpt2  5642  mptfvex  5644  elfvmptrab  5654  fvopab6  5655  f1ompt  5710  dfmpt  5736  ressnop0  5740  fprg  5742  fvsnun1  5756  fsnunfv  5760  fvpr2g  5766  imauni  5805  fliftfuns  5842  cbvriota  5885  oveq123i  5933  fconstmpo  6014  resoprab  6015  mpofun  6021  rnmpo  6030  reldmmpo  6031  ov  6039  ovigg  6040  ovmpt4g  6042  ovg  6059  caov31  6110  elmpocl  6115  f1ocnvd  6122  oprabrexex2  6184  op1st  6201  op2nd  6202  f1stres  6214  f2ndres  6215  unielxp  6229  dfoprab3s  6245  dfoprab4  6247  mpompts  6253  mpofvex  6260  oprab2co  6273  df1st2  6274  df2nd2  6275  f1od2  6290  brtpos0  6307  tposoprab  6335  smores3  6348  tfrlemi14d  6388  tfr1onlemaccex  6403  tfrcllemaccex  6416  rdgisuc1  6439  rdg0  6442  frec0g  6452  df1o2  6484  df2o2  6486  oasuc  6519  omv2  6520  omsuc  6527  ecidsn  6638  qliftfuns  6675  oviec  6697  mapsncnv  6751  dfixp  6756  xpcomco  6882  xpassen  6886  ssenen  6909  undifdc  6982  unfiin  6984  fidcenumlemrks  7014  fidcenumlemr  7016  sbthlemi5  7022  sbthlemi8  7025  fi0  7036  inf00  7092  djuf1olemr  7115  djuinr  7124  djuin  7125  djuun  7128  casefun  7146  casedm  7147  caseinj  7150  caseinl  7152  caseinr  7153  endjusym  7157  eninl  7158  eninr  7159  djudm  7166  djuinj  7167  fodjuomni  7210  fodjumkv  7221  nninfwlporlemd  7233  pm54.43  7252  exmidfodomrlemim  7263  xp2dju  7277  djucomen  7278  djuassen  7279  xpdjuen  7280  pw1nel3  7293  sucpw1nel3  7295  addpiord  7378  mulpiord  7379  dmaddpi  7387  dmmulpi  7388  recmulnqg  7453  1lt2nq  7468  halfnqq  7472  dfmq0qs  7491  dfplq0qs  7492  genpdf  7570  1prl  7617  1pru  7618  ltexprlemell  7660  ltexprlemelu  7661  recexprlemell  7684  recexprlemelu  7685  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdrl  7719  cauappcvgprlem2  7722  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem2  7742  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlem2  7772  addsrpr  7807  mulsrpr  7808  caucvgsrlemoffres  7862  caucvgsr  7864  suplocsrlempr  7869  addcnsr  7896  mulcnsr  7897  mulresr  7900  addvalex  7906  pitonnlem1  7907  axi2m1  7937  axcnre  7943  mulcomli  8028  mnfnre  8064  addcomli  8166  add42i  8187  mvrraddi  8238  neg0  8267  negdii  8305  negsubdi2i  8307  crap0  8979  2t2e4  9139  3t2e6  9141  3t3e9  9142  4t2e8  9143  neg1mulneg1e1  9197  8th4div3  9204  halfpm6th  9205  iap0  9208  dfdec10  9454  deceq12i  9459  numltc  9476  decsuc  9481  decsucc  9491  nummac  9495  numma2c  9496  numadd  9497  numaddc  9498  nummul1c  9499  nummul2c  9500  decma  9501  decmac  9502  decma2c  9503  decadd  9504  decaddc  9505  decrmanc  9507  decrmac  9508  decaddci  9511  decsubi  9513  decmul1  9514  decmul1c  9515  decmul2c  9516  11multnc  9518  4t3lem  9547  6t2e12  9554  7t2e14  9559  8t2e16  9565  9t2e18  9572  9t11e99  9580  halfthird  9593  5recm6rec  9594  divfnzn  9689  xnegpnf  9897  xneg0  9900  xaddmnf1  9917  xaddmnf2  9918  mnfaddpnf  9920  iooval2  9984  dfioo2  10043  fzval2  10080  fzsuc2  10148  fztpval  10152  fz0to3un2pr  10192  fz0to4untppr  10193  fzo01  10286  fzo12sn  10287  fzo0to42pr  10290  fldiv4p1lem1div2  10377  intqfrac2  10393  intfracq  10394  xnn0nnen  10511  1tonninf  10515  neg1sqe1  10708  sq2  10709  sq3  10710  cu2  10712  i2  10714  i3  10715  binom2i  10722  sq10  10786  3dec  10788  facp1  10804  fac2  10805  fac4  10807  4bc2eq6  10848  hashp1i  10884  pr0hash2ex  10889  hashfzo  10896  hashxp  10900  zfz1isolem1  10914  elovmpowrd  10958  cji  11049  cnrecnv  11057  sqrt0  11151  resqrexlemover  11157  resqrexlemcalc3  11163  absi  11206  absimle  11231  sumeq12i  11511  summodclem2a  11527  summodc  11529  sum0  11534  fsumsplitf  11554  fsum2dlemstep  11580  fsumabs  11611  fsumiun  11623  0.999...  11667  mertenslem2  11682  prodeq12i  11709  prodmodc  11724  fprod2dlemstep  11768  ege2le3  11817  eft0val  11839  cos0  11876  cos1bnd  11905  cos2bnd  11906  3dvdsdec  12009  3dvds2dec  12010  odd2np1  12017  opoe  12039  nn0o  12051  gcd0val  12100  6gcd4e2  12135  nnmindc  12174  nnminle  12175  3lcm2e6woprm  12227  3lcm2e6  12301  nn0gcdsq  12341  phiprmpw  12363  phimullem  12366  pcprecl  12430  pcprendvds  12431  pcmptdvds  12486  pockthi  12499  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  4sqlem18  12549  4sqlem19  12550  unennn  12557  ennnfonelemj0  12561  ennnfonelem0  12565  ennnfonelem1  12567  ennnfonelemhf1o  12573  ennnfonelemrn  12579  ennnfonelemdm  12580  strnfvnd  12641  slotslfn  12647  setsfun  12656  setsfun0  12657  setscom  12661  setsslid  12672  2strstr1g  12742  eqglact  13298  ecqusaddd  13311  ghmeqker  13344  dfrhm2  13653  rmodislmod  13850  cnfldadd  14061  cnfldmul  14063  expghmap  14106  fczpsrbag  14168  cnco  14400  txuni2  14435  txbas  14437  uptx  14453  txcn  14454  cnmptid  14460  cnmpt2t  14472  xmetxp  14686  cnmetdval  14708  remetdval  14726  resubmet  14735  rerestcntop  14737  rerest  14739  divcnap  14744  cnrehmeocntop  14789  dvexp  14890  plyun0  14915  plyco  14937  plycj  14939  sinhalfpilem  14967  cosneghalfpi  14974  efhalfpi  14975  cospi  14976  efipi  14977  eulerid  14978  sin2pi  14979  cos2pi  14980  ef2pi  14981  sincosq4sgn  15005  cosq14gt0  15008  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  sinkpi  15023  cosq34lt1  15026  dfrelog  15036  2logb9irr  15144  2logb9irrALT  15147  2logb9irrap  15150  zabsle1  15156  lgslem2  15158  lgsfcl2  15163  lgsdir2lem1  15185  lgsdir2lem2  15186  lgsdir2lem4  15188  lgsdir2lem5  15189  lgseisen  15231  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgs2  15259  2lgsoddprmlem3a  15264  2lgsoddprmlem3b  15265  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  ex-fl  15287  ex-exp  15289  ex-fac  15290  ex-bc  15291  ex-dvds  15292  ex-gcd  15293  bj-dfom  15495  012of  15556  2o01f  15557  pwle2  15559  nninfsellemqall  15575  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612  dceqnconst  15620  dcapnconst  15621  taupi  15633