Theorem eqtri 2255

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 2245	. 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 2216

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

This theorem is referenced by:  eqtr2i  2256  eqtr3i  2257  eqtr4i  2258  3eqtri  2259  3eqtrri  2260  3eqtr2i  2261  cbvrab  2813  csb2  3143  cbvrabcsf  3207  difjust  3215  unjust  3217  injust  3219  dfdif3  3333  difeq12i  3339  ineqcomi  3417  inrot  3440  symdif1  3490  rabnc  3545  0in  3548  ssdifin0  3595  dfif3  3640  ifbieq2i  3650  ifbieq12i  3652  pwjust  3675  snjust  3699  dfpr2  3713  disjpr2  3758  rabsnifsb  3762  difprsn1  3838  diftpsn3  3840  difpr  3841  dfuni2  3921  intab  3983  intunsn  3992  rint0  3993  iunid  4052  viin  4056  iinrabm  4059  2iunin  4063  riin0  4068  iunxprg  4077  unopab  4194  cbvmptf  4209  cbvmpt  4210  exmid1stab  4326  unisucg  4540  op1stb  4604  orddif  4674  elxpi  4770  csbxpg  4836  relopabi  4885  inxp  4894  coeq12i  4923  dfdm3  4947  dfrn3  4949  dmun  4968  dmopab  4972  dmopab3  4974  dmxpid  4983  dmxpin  4984  rnopab  5009  rnmpt  5010  rncoss  5033  rncoeq  5036  reseq12i  5041  resundi  5056  resindi  5058  resiun1  5062  resdmdfsn  5086  resopab  5087  opabresid  5096  dfima3  5109  mptima  5118  imadisj  5129  ndmima  5144  mptcnv  5170  rnun  5176  rnuni  5179  imaundi  5180  inimass  5184  cnvxp  5186  rnxpm  5197  dminxp  5212  imainrect  5213  cnvcnv3  5217  dmpropg  5240  op1sta  5249  op2ndb  5251  op2nda  5252  resdmres  5259  mptpreima  5261  coundi  5269  coundir  5270  cocnvcnv1  5278  cores2  5280  dfdm2  5302  iotajust  5316  dfiota2  5318  funi  5389  funtp  5414  fntpg  5417  funcnvuni  5430  funcnvres  5434  imadiflem  5440  imadif  5441  imainlem  5442  imain  5443  fnresdisj  5473  mptfng  5489  fresaunres2disj  5550  resdif  5641  fv2  5670  dffv4g  5672  fveq12i  5681  nfvres  5711  0fv  5713  dfimafn2  5731  fnimapr  5742  fvmptss2  5757  fvmptg  5758  fvmpts  5760  fvmpt2  5766  mptfvex  5768  elfvmptrab  5778  fvopab6  5779  f1ompt  5833  dfmpt  5860  ressnop0  5870  fprg  5872  fvsnun1  5886  fsnunfv  5890  fvpr2g  5896  imauni  5940  fliftfuns  5977  cbvriota  6023  oveq123i  6072  fconstmpo  6156  resoprab  6157  mpofun  6163  rnmpo  6172  reldmmpo  6173  ov  6181  ovigg  6182  ovmpt4g  6184  ovg  6201  caov31  6252  elmpocl  6257  f1ocnvd  6265  oprabrexex2  6336  op1st  6353  op2nd  6354  f1stres  6366  f2ndres  6367  unielxp  6381  dfoprab3s  6397  dfoprab4  6399  mpompts  6407  mpofvex  6414  oprab2co  6427  df1st2  6428  df2nd2  6429  f1od2  6444  elmpom  6447  cnvimadfsn  6458  brtpos0  6496  tposoprab  6524  smores3  6537  tfrlemi14d  6577  tfr1onlemaccex  6592  tfrcllemaccex  6605  rdgisuc1  6628  rdg0  6631  frec0g  6641  df1o2  6674  df2o2  6676  oasuc  6710  omv2  6711  omsuc  6718  ecidsn  6829  qliftfuns  6866  oviec  6888  mapsncnv  6943  dfixp  6948  xpcomco  7090  xpassen  7094  ssenen  7118  undifdc  7197  unfiin  7199  fidcenumlemrks  7236  fidcenumlemr  7238  sbthlemi5  7244  sbthlemi8  7247  fi0  7275  inf00  7335  djuf1olemr  7358  djuinr  7367  djuin  7368  djuun  7371  casefun  7389  casedm  7390  caseinj  7393  caseinl  7395  caseinr  7396  endjusym  7400  eninl  7401  eninr  7402  djudm  7409  djuinj  7410  fodjuomni  7453  fodjumkv  7464  nninfwlporlemd  7476  pm54.43  7500  exmidfodomrlemim  7517  xp2dju  7535  djucomen  7536  djuassen  7537  xpdjuen  7538  pw1nel3  7554  sucpw1nel3  7556  addpiord  7647  mulpiord  7648  dmaddpi  7656  dmmulpi  7657  recmulnqg  7722  1lt2nq  7737  halfnqq  7741  dfmq0qs  7760  dfplq0qs  7761  genpdf  7839  1prl  7886  1pru  7887  ltexprlemell  7929  ltexprlemelu  7930  recexprlemell  7953  recexprlemelu  7954  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem2  8041  addsrpr  8076  mulsrpr  8077  caucvgsrlemoffres  8131  caucvgsr  8133  suplocsrlempr  8138  addcnsr  8165  mulcnsr  8166  mulresr  8169  addvalex  8175  pitonnlem1  8176  axi2m1  8206  axcnre  8212  mulcomli  8297  mnfnre  8332  addcomli  8435  add42i  8456  mvrraddi  8507  neg0  8536  negdii  8574  negsubdi2i  8576  crap0  9252  2t2e4  9412  3t2e6  9414  3t3e9  9415  4t2e8  9416  neg1mulneg1e1  9470  8th4div3  9477  halfpm6th  9478  iap0  9481  dfdec10  9733  deceq12i  9738  numltc  9755  decsuc  9760  decsucc  9770  nummac  9774  numma2c  9775  numadd  9776  numaddc  9777  nummul1c  9778  nummul2c  9779  decma  9780  decmac  9781  decma2c  9782  decadd  9783  decaddc  9784  decrmanc  9786  decrmac  9787  decaddci  9790  decsubi  9792  decmul1  9793  decmul1c  9794  decmul2c  9795  11multnc  9797  4t3lem  9826  6t2e12  9833  7t2e14  9838  8t2e16  9844  9t2e18  9851  9t11e99  9859  halfthird  9872  5recm6rec  9873  divfnzn  9974  xnegpnf  10183  xneg0  10186  xaddmnf1  10203  xaddmnf2  10204  mnfaddpnf  10206  iooval2  10270  dfioo2  10329  fzval2  10367  fzsuc2  10438  fztpval  10442  fz0to3un2pr  10482  fz0to4untppr  10483  fzo01  10586  fzo12sn  10587  fzo0to42pr  10590  fldiv4p1lem1div2  10692  intqfrac2  10708  intfracq  10709  xnn0nnen  10826  1tonninf  10830  neg1sqe1  11023  sq2  11024  sq3  11025  cu2  11027  i2  11029  i3  11030  binom2i  11037  sq10  11102  3dec  11104  facp1  11120  fac2  11121  fac4  11123  4bc2eq6  11165  hashp1i  11203  pr0hash2ex  11208  hashfzo  11215  hashxp  11219  hashfibclem  11234  zfz1isolem1  11240  elovmpowrd  11294  ccat1st1st  11357  cji  11616  cnrecnv  11624  sqrt0  11718  resqrexlemover  11724  resqrexlemcalc3  11730  absi  11773  absimle  11798  sumeq12i  12079  summodclem2a  12096  summodc  12098  sum0  12103  fsumsplitf  12123  fsum2dlemstep  12149  fsumabs  12180  fsumiun  12192  0.999...  12236  mertenslem2  12251  prodeq12i  12278  prodmodc  12293  fprod2dlemstep  12337  ege2le3  12386  eft0val  12408  cos0  12445  cos1bnd  12474  cos2bnd  12475  3dvdsdec  12580  3dvds2dec  12581  odd2np1  12588  opoe  12610  nn0o  12622  5ndvds3  12649  5ndvds6  12650  bitsfzolem  12669  m1bits  12675  gcd0val  12685  6gcd4e2  12720  nnmindc  12759  nnminle  12760  3lcm2e6woprm  12812  3lcm2e6  12886  nn0gcdsq  12926  phiprmpw  12948  phimullem  12951  pcprecl  13016  pcprendvds  13017  pcmptdvds  13072  pockthi  13085  4sqlem13m  13130  4sqlem14  13131  4sqlem17  13134  4sqlem18  13135  4sqlem19  13136  dec5nprm  13141  dec2nprm  13142  modxai  13143  modsubi  13146  numexp2x  13152  decsplit0b  13153  decsplit0  13154  decsplit  13156  karatsuba  13157  2exp5  13159  2exp7  13161  2exp8  13162  2exp11  13163  2exp16  13164  3exp3  13165  ballotfilemelo  13170  ballotfilem2  13176  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemfval0  13183  ballotfileme  13184  ballotfilemi  13191  ballotfilemsval  13200  ballotfilemrval  13209  ballotfilemrinv  13225  ballotfilemth  13229  ballotfi  13230  unennn  13236  ennnfonelemj0  13240  ennnfonelem0  13244  ennnfonelem1  13246  ennnfonelemhf1o  13252  ennnfonelemrn  13258  ennnfonelemdm  13259  strnfvnd  13320  slotslfn  13326  setsfun  13335  setsfun0  13336  setscom  13340  setsslid  13351  2strstr1g  13423  eqglact  13982  ecqusaddd  13995  ghmeqker  14028  gfsump1  14112  dfrhm2  14403  rmodislmod  14629  cnfldadd  14840  cnfldmul  14842  expghmap  14885  fczpsrbag  14950  cnco  15216  txuni2  15251  txbas  15253  uptx  15269  txcn  15270  cnmptid  15276  cnmpt2t  15288  xmetxp  15502  cnmetdval  15524  remetdval  15542  resubmet  15551  rerestcntop  15553  rerest  15555  divcnap  15560  cnrehmeocntop  15605  dvexp  15706  plyun0  15731  plyco  15754  plycj  15756  sinhalfpilem  15786  cosneghalfpi  15793  efhalfpi  15794  cospi  15795  efipi  15796  eulerid  15797  sin2pi  15798  cos2pi  15799  ef2pi  15800  sincosq4sgn  15824  cosq14gt0  15827  tangtx  15833  sincos4thpi  15835  sincos6thpi  15837  sinkpi  15842  cosq34lt1  15845  dfrelog  15855  2logb9irr  15966  2logb9irrALT  15969  2logb9irrap  15972  mersenne  15995  perfectlem2  15998  zabsle1  16002  lgslem2  16004  lgsfcl2  16009  lgsdir2lem1  16031  lgsdir2lem2  16032  lgsdir2lem4  16034  lgsdir2lem5  16035  lgseisen  16077  2lgslem3a  16096  2lgslem3b  16097  2lgslem3c  16098  2lgslem3d  16099  2lgs2  16105  2lgsoddprmlem3a  16110  2lgsoddprmlem3b  16111  2lgsoddprmlem3c  16112  2lgsoddprmlem3d  16113  pw0ss  16208  umgrislfupgrenlem  16255  vtxdgfval  16413  clwwlknon2  16559  clwwlknon2x  16560  eupth2lembfi  16602  konigsbergvtx  16607  konigsbergiedg  16608  konigsberglem1  16613  konigsberglem2  16614  konigsberglem3  16615  ex-fl  16623  ex-exp  16625  ex-fac  16626  ex-bc  16627  ex-dvds  16628  ex-gcd  16629  bj-dfom  16843  012of  16907  2o01f  16908  pwle2  16912  nninfsellemqall  16933  isomninnlem  16954  iswomninnlem  16974  ismkvnnlem  16977  dceqnconst  16985  dcapnconst  16986  taupi  16998