Theorem eqtri 2259

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2i  2260  eqtr3i  2261  eqtr4i  2262  3eqtri  2263  3eqtrri  2264  3eqtr2i  2265  cbvrab  2819  csb2  3149  cbvrabcsf  3213  difjust  3221  unjust  3223  injust  3225  dfdif3  3339  difeq12i  3345  ineqcomi  3423  inrot  3446  symdif1  3496  rabnc  3555  0in  3558  ssdifin0  3609  dfif3  3654  ifbieq2i  3664  ifbieq12i  3666  pwjust  3689  snjust  3714  dfpr2  3728  disjpr2  3773  rabsnifsb  3777  difprsn1  3854  diftpsn3  3856  difpr  3857  dfuni2  3937  intab  3999  intunsn  4008  rint0  4009  iunid  4068  viin  4072  iinrabm  4075  2iunin  4079  riin0  4084  iunxprg  4093  unopab  4210  cbvmptf  4225  cbvmpt  4226  exmid1stab  4345  unisucg  4559  op1stb  4624  orddif  4694  elxpi  4790  csbxpg  4856  relopabi  4905  inxp  4914  coeq12i  4943  dfdm3  4967  dfrn3  4969  dmun  4988  dmopab  4992  dmopab3  4994  dmxpid  5003  dmxpin  5004  rnopab  5029  rnmpt  5030  rncoss  5053  rncoeq  5056  reseq12i  5061  resundi  5076  resindi  5078  resiun1  5082  resdmdfsn  5106  resopab  5107  opabresid  5116  dfima3  5129  mptima  5138  imadisj  5149  ndmima  5164  mptcnv  5190  rnun  5196  rnuni  5199  imaundi  5200  inimass  5204  cnvxp  5206  rnxpm  5217  dminxp  5232  imainrect  5233  cnvcnv3  5237  dmpropg  5260  op1sta  5269  op2ndb  5271  op2nda  5272  resdmres  5279  mptpreima  5281  coundi  5289  coundir  5290  cocnvcnv1  5298  cores2  5300  dfdm2  5322  iotajust  5336  dfiota2  5338  funi  5409  funtp  5434  fntpg  5437  funcnvuni  5450  funcnvres  5454  imadiflem  5460  imadif  5461  imainlem  5462  imain  5463  fnresdisj  5493  mptfng  5509  fresaunres2disj  5570  resdif  5661  fv2  5690  dffv4g  5692  fveq12i  5701  nfvres  5732  0fv  5734  dfimafn2  5752  fnimapr  5763  fvmptss2  5780  fvmptg  5781  fvmpts  5783  fvmpt2  5789  mptfvex  5791  elfvmptrab  5802  fvmptndm  5804  fvopab6  5805  f1ompt  5859  dfmpt  5886  ressnop0  5896  fprg  5898  fvsnun1  5912  fsnunfv  5916  fvpr2g  5922  imauni  5967  fliftfuns  6004  cbvriota  6050  oveq123i  6099  fconstmpo  6183  resoprab  6184  mpofun  6190  rnmpo  6199  reldmmpo  6200  ov  6208  ovigg  6209  ovmpt4g  6211  ovg  6228  caov31  6279  elmpocl  6284  f1ocnvd  6292  oprabrexex2  6363  op1st  6380  op2nd  6381  f1stres  6393  f2ndres  6394  unielxp  6408  dfoprab3s  6424  dfoprab4  6426  mpompts  6434  mpofvex  6441  oprab2co  6454  df1st2  6455  df2nd2  6456  f1od2  6471  elmpom  6474  cnvimadfsn  6485  brtpos0  6523  tposoprab  6551  smores3  6564  tfrlemi14d  6604  tfr1onlemaccex  6619  tfrcllemaccex  6632  rdgisuc1  6655  rdg0  6658  frec0g  6668  df1o2  6701  df2o2  6703  oasuc  6737  omv2  6738  omsuc  6745  ecidsn  6856  qliftfuns  6893  oviec  6915  mapsncnv  6977  dfixp  6982  xpcomco  7124  xpassen  7128  ssenen  7152  undifdc  7231  unfiin  7233  fidcenumlemrks  7270  fidcenumlemr  7272  sbthlemi5  7278  sbthlemi8  7281  fi0  7309  inf00  7371  djuf1olemr  7394  djuinr  7403  djuin  7404  djuun  7407  casefun  7425  casedm  7426  caseinj  7429  caseinl  7431  caseinr  7432  endjusym  7436  eninl  7437  eninr  7438  djudm  7445  djuinj  7446  fodjuomni  7489  fodjumkv  7500  nninfwlporlemd  7512  pm54.43  7536  exmidfodomrlemim  7553  xp2dju  7571  djucomen  7572  djuassen  7573  xpdjuen  7574  pw1nel3  7590  sucpw1nel3  7592  addpiord  7683  mulpiord  7684  dmaddpi  7692  dmmulpi  7693  recmulnqg  7758  1lt2nq  7773  halfnqq  7777  dfmq0qs  7796  dfplq0qs  7797  genpdf  7875  1prl  7922  1pru  7923  ltexprlemell  7965  ltexprlemelu  7966  recexprlemell  7989  recexprlemelu  7990  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem2  8047  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem2  8077  addsrpr  8112  mulsrpr  8113  caucvgsrlemoffres  8167  caucvgsr  8169  suplocsrlempr  8174  addcnsr  8201  mulcnsr  8202  mulresr  8205  addvalex  8211  pitonnlem1  8212  axi2m1  8242  axcnre  8248  mulcomli  8333  mnfnre  8368  addcomli  8471  add42i  8492  mvrraddi  8543  neg0  8572  negdii  8610  negsubdi2i  8612  crap0  9289  2t2e4  9460  3t2e6  9462  3t3e9  9464  4t2e8  9465  neg1mulneg1e1  9519  8th4div3  9526  halfpm6th  9527  iap0  9530  dfdec10  9782  deceq12i  9787  numltc  9804  decsuc  9809  decsucc  9819  nummac  9823  numma2c  9824  numadd  9825  numaddc  9826  nummul1c  9827  nummul2c  9828  decma  9829  decmac  9830  decma2c  9831  decadd  9832  decaddc  9833  decrmanc  9835  decrmac  9836  decaddci  9839  decsubi  9841  decmul1  9842  decmul1c  9843  decmul2c  9844  11multnc  9846  4t3lem  9875  6t2e12  9882  7t2e14  9887  8t2e16  9893  9t2e18  9900  9t11e99  9908  halfthird  9921  5recm6rec  9922  divfnzn  10023  xnegpnf  10232  xneg0  10235  xaddmnf1  10252  xaddmnf2  10253  mnfaddpnf  10255  iooval2  10319  dfioo2  10378  fzval2  10416  fzsuc2  10488  fztpval  10492  fz0to3un2pr  10532  fz0to4untppr  10533  fzo01  10636  fzo12sn  10637  fzo0to42pr  10640  fldiv4p1lem1div2  10742  intqfrac2  10758  intfracq  10759  xnn0nnen  10876  1tonninf  10880  neg1sqe1  11073  sq2  11074  sq3  11075  cu2  11077  i2  11079  i3  11080  binom2i  11087  sq10  11152  3dec  11154  facp1  11170  fac2  11171  fac4  11173  4bc2eq6  11215  hashp1i  11253  pr0hash2ex  11258  hashfzo  11265  hashxp  11269  hashfibclem  11284  zfz1isolem1  11294  elovmpowrd  11348  ccat1st1st  11411  cji  11670  cnrecnv  11678  sqrt0  11772  resqrexlemover  11778  resqrexlemcalc3  11784  absi  11827  absimle  11852  sumeq12i  12133  summodclem2a  12150  summodc  12152  sum0  12157  fsumsplitf  12177  fsum2dlemstep  12203  fsumabs  12234  fsumiun  12246  0.999...  12290  mertenslem2  12305  prodeq12i  12332  prodmodc  12347  fprod2dlemstep  12391  ege2le3  12440  eft0val  12462  cos0  12499  cos1bnd  12528  cos2bnd  12529  3dvdsdec  12634  3dvds2dec  12635  odd2np1  12642  opoe  12664  nn0o  12676  5ndvds3  12703  5ndvds6  12704  bitsfzolem  12723  m1bits  12729  gcd0val  12739  6gcd4e2  12774  nnmindc  12813  nnminle  12814  3lcm2e6woprm  12866  3lcm2e6  12940  nn0gcdsq  12980  phiprmpw  13002  phimullem  13005  pcprecl  13070  pcprendvds  13071  pcmptdvds  13126  pockthi  13139  4sqlem13m  13184  4sqlem14  13185  4sqlem17  13188  4sqlem18  13189  4sqlem19  13190  dec5nprm  13195  dec2nprm  13196  modxai  13197  modsubi  13200  numexp2x  13206  decsplit0b  13207  decsplit0  13208  decsplit  13210  karatsuba  13211  2exp5  13213  2exp7  13215  2exp8  13216  2exp11  13217  2exp16  13218  3exp3  13219  ballotfilemelo  13224  ballotfilem2  13230  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemfval0  13237  ballotfileme  13238  ballotfilemi  13245  ballotfilemsval  13254  ballotfilemrval  13263  ballotfilemrinv  13279  ballotfilemth  13283  ballotfi  13284  unennn  13290  ennnfonelemj0  13294  ennnfonelem0  13298  ennnfonelem1  13300  ennnfonelemhf1o  13306  ennnfonelemrn  13312  ennnfonelemdm  13313  strnfvnd  13374  slotslfn  13380  setsfun  13389  setsfun0  13390  setscom  13394  setsslid  13405  2strstr1g  13478  eqglact  14030  ecqusaddd  14043  ghmeqker  14076  dfrhm2  14463  rmodislmod  14690  cnfldadd  14901  cnfldmul  14903  gsumfsum  14925  expghmap  14944  asclfval  15023  fczpsrbag  15058  cnco  15324  txuni2  15359  txbas  15361  uptx  15377  txcn  15378  cnmptid  15384  cnmpt2t  15396  xmetxp  15610  cnmetdval  15632  remetdval  15650  resubmet  15659  rerestcntop  15661  rerest  15663  divcnap  15668  cnrehmeocntop  15713  dvexp  15814  plyun0  15839  plyco  15862  plycj  15864  sinhalfpilem  15895  cosneghalfpi  15902  efhalfpi  15903  cospi  15904  efipi  15905  eulerid  15906  sin2pi  15907  cos2pi  15908  ef2pi  15909  sincosq4sgn  15933  cosq14gt0  15936  tangtx  15942  sincos4thpi  15944  sincos6thpi  15946  sinkpi  15951  cosq34lt1  15954  dfrelog  15964  2logb9irr  16079  2logb9irrALT  16082  2logb9irrap  16085  log2tlbndlog2  16088  log2ublem2  16090  log2ublem3  16091  log2ublog2  16092  birthdaylem2  16094  birthdaylog2  16096  mersenne  16117  perfectlem2  16120  bcp1ctr  16126  bclbnd  16127  zabsle1  16130  lgslem2  16132  lgsfcl2  16137  lgsdir2lem1  16159  lgsdir2lem2  16160  lgsdir2lem4  16162  lgsdir2lem5  16163  lgseisen  16205  2lgslem3a  16224  2lgslem3b  16225  2lgslem3c  16226  2lgslem3d  16227  2lgs2  16233  2lgsoddprmlem3a  16238  2lgsoddprmlem3b  16239  2lgsoddprmlem3c  16240  2lgsoddprmlem3d  16241  pw0ss  16336  umgrislfupgrenlem  16383  vtxdgfval  16541  clwwlknon2  16687  clwwlknon2x  16688  eupth2lembfi  16730  konigsbergvtx  16735  konigsbergiedg  16736  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  ex-fl  16751  ex-exp  16753  ex-fac  16754  ex-bc  16755  ex-dvds  16756  ex-gcd  16757  bj-dfom  16971  012of  17035  2o01f  17036  pwle2  17040  nninfsellemqall  17070  isomninnlem  17091  iswomninnlem  17111  ismkvnnlem  17114  dceqnconst  17122  dcapnconst  17123  taupi  17135