Theorem eqtri 2253

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 2243	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐴 = 𝐶)
4	1, 3	mpbi 145	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  eqtr2i  2254  eqtr3i  2255  eqtr4i  2256  3eqtri  2257  3eqtrri  2258  3eqtr2i  2259  cbvrab  2810  csb2  3139  cbvrabcsf  3203  difjust  3211  unjust  3213  injust  3215  dfdif3  3328  difeq12i  3334  ineqcomi  3412  inrot  3435  symdif1  3485  rabnc  3540  0in  3543  ssdifin0  3590  dfif3  3635  ifbieq2i  3645  ifbieq12i  3647  pwjust  3669  snjust  3693  dfpr2  3707  disjpr2  3752  rabsnifsb  3756  difprsn1  3832  diftpsn3  3834  difpr  3835  dfuni2  3915  intab  3977  intunsn  3986  rint0  3987  iunid  4046  viin  4050  iinrabm  4053  2iunin  4057  riin0  4062  iunxprg  4071  unopab  4188  cbvmptf  4203  cbvmpt  4204  exmid1stab  4320  unisucg  4534  op1stb  4598  orddif  4668  elxpi  4764  csbxpg  4830  relopabi  4879  inxp  4888  coeq12i  4917  dfdm3  4941  dfrn3  4943  dmun  4962  dmopab  4966  dmopab3  4968  dmxpid  4977  dmxpin  4978  rnopab  5003  rnmpt  5004  rncoss  5027  rncoeq  5030  reseq12i  5035  resundi  5050  resindi  5052  resiun1  5056  resdmdfsn  5080  resopab  5081  opabresid  5090  dfima3  5103  mptima  5112  imadisj  5123  ndmima  5138  mptcnv  5164  rnun  5170  rnuni  5173  imaundi  5174  inimass  5178  cnvxp  5180  rnxpm  5191  dminxp  5206  imainrect  5207  cnvcnv3  5211  dmpropg  5234  op1sta  5243  op2ndb  5245  op2nda  5246  resdmres  5253  mptpreima  5255  coundi  5263  coundir  5264  cocnvcnv1  5272  cores2  5274  dfdm2  5296  iotajust  5310  dfiota2  5312  funi  5383  funtp  5408  fntpg  5411  funcnvuni  5424  funcnvres  5428  imadiflem  5434  imadif  5435  imainlem  5436  imain  5437  fnresdisj  5467  mptfng  5483  fresaunres2disj  5544  resdif  5635  fv2  5664  dffv4g  5666  fveq12i  5675  nfvres  5705  0fv  5707  dfimafn2  5725  fnimapr  5736  fvmptss2  5751  fvmptg  5752  fvmpts  5754  fvmpt2  5760  mptfvex  5762  elfvmptrab  5772  fvopab6  5773  f1ompt  5827  dfmpt  5854  ressnop0  5864  fprg  5866  fvsnun1  5880  fsnunfv  5884  fvpr2g  5890  imauni  5933  fliftfuns  5970  cbvriota  6014  oveq123i  6063  fconstmpo  6147  resoprab  6148  mpofun  6154  rnmpo  6163  reldmmpo  6164  ov  6172  ovigg  6173  ovmpt4g  6175  ovg  6192  caov31  6243  elmpocl  6248  f1ocnvd  6256  oprabrexex2  6322  op1st  6339  op2nd  6340  f1stres  6352  f2ndres  6353  unielxp  6367  dfoprab3s  6383  dfoprab4  6385  mpompts  6393  mpofvex  6400  oprab2co  6413  df1st2  6414  df2nd2  6415  f1od2  6430  elmpom  6433  cnvimadfsn  6444  brtpos0  6482  tposoprab  6510  smores3  6523  tfrlemi14d  6563  tfr1onlemaccex  6578  tfrcllemaccex  6591  rdgisuc1  6614  rdg0  6617  frec0g  6627  df1o2  6660  df2o2  6662  oasuc  6696  omv2  6697  omsuc  6704  ecidsn  6815  qliftfuns  6852  oviec  6874  mapsncnv  6929  dfixp  6934  xpcomco  7076  xpassen  7080  ssenen  7104  undifdc  7183  unfiin  7185  fidcenumlemrks  7222  fidcenumlemr  7224  sbthlemi5  7230  sbthlemi8  7233  fi0  7261  inf00  7321  djuf1olemr  7344  djuinr  7353  djuin  7354  djuun  7357  casefun  7375  casedm  7376  caseinj  7379  caseinl  7381  caseinr  7382  endjusym  7386  eninl  7387  eninr  7388  djudm  7395  djuinj  7396  fodjuomni  7439  fodjumkv  7450  nninfwlporlemd  7462  pm54.43  7486  exmidfodomrlemim  7503  xp2dju  7521  djucomen  7522  djuassen  7523  xpdjuen  7524  pw1nel3  7540  sucpw1nel3  7542  addpiord  7630  mulpiord  7631  dmaddpi  7639  dmmulpi  7640  recmulnqg  7705  1lt2nq  7720  halfnqq  7724  dfmq0qs  7743  dfplq0qs  7744  genpdf  7822  1prl  7869  1pru  7870  ltexprlemell  7912  ltexprlemelu  7913  recexprlemell  7936  recexprlemelu  7937  cauappcvgprlemm  7959  cauappcvgprlemopl  7960  cauappcvgprlemlol  7961  cauappcvgprlemopu  7962  cauappcvgprlemupu  7963  cauappcvgprlemdisj  7965  cauappcvgprlemloc  7966  cauappcvgprlemladdfu  7968  cauappcvgprlemladdfl  7969  cauappcvgprlemladdrl  7971  cauappcvgprlem2  7974  caucvgprlemm  7982  caucvgprlemopl  7983  caucvgprlemlol  7984  caucvgprlemopu  7985  caucvgprlemupu  7986  caucvgprlemdisj  7988  caucvgprlemloc  7989  caucvgprlemcl  7990  caucvgprlemladdfu  7991  caucvgprlemladdrl  7992  caucvgprlem2  7994  caucvgprprlemell  7999  caucvgprprlemelu  8000  caucvgprprlemml  8008  caucvgprprlemmu  8009  caucvgprprlemclphr  8019  caucvgprprlemexbt  8020  caucvgprprlem2  8024  addsrpr  8059  mulsrpr  8060  caucvgsrlemoffres  8114  caucvgsr  8116  suplocsrlempr  8121  addcnsr  8148  mulcnsr  8149  mulresr  8152  addvalex  8158  pitonnlem1  8159  axi2m1  8189  axcnre  8195  mulcomli  8280  mnfnre  8315  addcomli  8417  add42i  8438  mvrraddi  8489  neg0  8518  negdii  8556  negsubdi2i  8558  crap0  9231  2t2e4  9391  3t2e6  9393  3t3e9  9394  4t2e8  9395  neg1mulneg1e1  9449  8th4div3  9456  halfpm6th  9457  iap0  9460  dfdec10  9711  deceq12i  9716  numltc  9733  decsuc  9738  decsucc  9748  nummac  9752  numma2c  9753  numadd  9754  numaddc  9755  nummul1c  9756  nummul2c  9757  decma  9758  decmac  9759  decma2c  9760  decadd  9761  decaddc  9762  decrmanc  9764  decrmac  9765  decaddci  9768  decsubi  9770  decmul1  9771  decmul1c  9772  decmul2c  9773  11multnc  9775  4t3lem  9804  6t2e12  9811  7t2e14  9816  8t2e16  9822  9t2e18  9829  9t11e99  9837  halfthird  9850  5recm6rec  9851  divfnzn  9952  xnegpnf  10160  xneg0  10163  xaddmnf1  10180  xaddmnf2  10181  mnfaddpnf  10183  iooval2  10247  dfioo2  10306  fzval2  10344  fzsuc2  10412  fztpval  10416  fz0to3un2pr  10456  fz0to4untppr  10457  fzo01  10560  fzo12sn  10561  fzo0to42pr  10564  fldiv4p1lem1div2  10664  intqfrac2  10680  intfracq  10681  xnn0nnen  10798  1tonninf  10802  neg1sqe1  10995  sq2  10996  sq3  10997  cu2  10999  i2  11001  i3  11002  binom2i  11009  sq10  11073  3dec  11075  facp1  11091  fac2  11092  fac4  11094  4bc2eq6  11135  hashp1i  11173  pr0hash2ex  11178  hashfzo  11185  hashxp  11189  hashfibclem  11202  zfz1isolem1  11208  elovmpowrd  11262  ccat1st1st  11325  cji  11583  cnrecnv  11591  sqrt0  11685  resqrexlemover  11691  resqrexlemcalc3  11697  absi  11740  absimle  11765  sumeq12i  12046  summodclem2a  12063  summodc  12065  sum0  12070  fsumsplitf  12090  fsum2dlemstep  12116  fsumabs  12147  fsumiun  12159  0.999...  12203  mertenslem2  12218  prodeq12i  12245  prodmodc  12260  fprod2dlemstep  12304  ege2le3  12353  eft0val  12375  cos0  12412  cos1bnd  12441  cos2bnd  12442  3dvdsdec  12547  3dvds2dec  12548  odd2np1  12555  opoe  12577  nn0o  12589  5ndvds3  12616  5ndvds6  12617  bitsfzolem  12636  m1bits  12642  gcd0val  12652  6gcd4e2  12687  nnmindc  12726  nnminle  12727  3lcm2e6woprm  12779  3lcm2e6  12853  nn0gcdsq  12893  phiprmpw  12915  phimullem  12918  pcprecl  12983  pcprendvds  12984  pcmptdvds  13039  pockthi  13052  4sqlem13m  13097  4sqlem14  13098  4sqlem17  13101  4sqlem18  13102  4sqlem19  13103  dec5nprm  13108  dec2nprm  13109  modxai  13110  modsubi  13113  numexp2x  13119  decsplit0b  13120  decsplit0  13121  decsplit  13123  karatsuba  13124  2exp5  13126  2exp7  13128  2exp8  13129  2exp11  13130  2exp16  13131  3exp3  13132  unennn  13140  ennnfonelemj0  13144  ennnfonelem0  13148  ennnfonelem1  13150  ennnfonelemhf1o  13156  ennnfonelemrn  13162  ennnfonelemdm  13163  strnfvnd  13224  slotslfn  13230  setsfun  13239  setsfun0  13240  setscom  13244  setsslid  13255  2strstr1g  13327  eqglact  13934  ecqusaddd  13947  ghmeqker  13980  dfrhm2  14291  rmodislmod  14491  cnfldadd  14702  cnfldmul  14704  expghmap  14747  fczpsrbag  14812  cnco  15078  txuni2  15113  txbas  15115  uptx  15131  txcn  15132  cnmptid  15138  cnmpt2t  15150  xmetxp  15364  cnmetdval  15386  remetdval  15404  resubmet  15413  rerestcntop  15415  rerest  15417  divcnap  15422  cnrehmeocntop  15467  dvexp  15568  plyun0  15593  plyco  15616  plycj  15618  sinhalfpilem  15648  cosneghalfpi  15655  efhalfpi  15656  cospi  15657  efipi  15658  eulerid  15659  sin2pi  15660  cos2pi  15661  ef2pi  15662  sincosq4sgn  15686  cosq14gt0  15689  tangtx  15695  sincos4thpi  15697  sincos6thpi  15699  sinkpi  15704  cosq34lt1  15707  dfrelog  15717  2logb9irr  15828  2logb9irrALT  15831  2logb9irrap  15834  mersenne  15857  perfectlem2  15860  zabsle1  15864  lgslem2  15866  lgsfcl2  15871  lgsdir2lem1  15893  lgsdir2lem2  15894  lgsdir2lem4  15896  lgsdir2lem5  15897  lgseisen  15939  2lgslem3a  15958  2lgslem3b  15959  2lgslem3c  15960  2lgslem3d  15961  2lgs2  15967  2lgsoddprmlem3a  15972  2lgsoddprmlem3b  15973  2lgsoddprmlem3c  15974  2lgsoddprmlem3d  15975  pw0ss  16070  umgrislfupgrenlem  16117  vtxdgfval  16275  clwwlknon2  16421  clwwlknon2x  16422  eupth2lembfi  16464  konigsbergvtx  16469  konigsbergiedg  16470  konigsberglem1  16475  konigsberglem2  16476  konigsberglem3  16477  ex-fl  16485  ex-exp  16487  ex-fac  16488  ex-bc  16489  ex-dvds  16490  ex-gcd  16491  bj-dfom  16695  012of  16759  2o01f  16760  pwle2  16764  nninfsellemqall  16785  isomninnlem  16806  iswomninnlem  16826  ismkvnnlem  16829  dceqnconst  16837  dcapnconst  16838  taupi  16850  gfsump1  16859