Theorem eqtri 2250

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtr2i  2251  eqtr3i  2252  eqtr4i  2253  3eqtri  2254  3eqtrri  2255  3eqtr2i  2256  cbvrab  2798  csb2  3127  cbvrabcsf  3191  difjust  3199  unjust  3201  injust  3203  dfdif3  3315  difeq12i  3321  inrot  3420  symdif1  3470  rabnc  3525  0in  3528  ssdifin0  3574  dfif3  3617  ifbieq2i  3627  ifbieq12i  3629  pwjust  3651  snjust  3672  dfpr2  3686  disjpr2  3731  rabsnifsb  3735  difprsn1  3810  diftpsn3  3812  difpr  3813  dfuni2  3893  intab  3955  intunsn  3964  rint0  3965  iunid  4024  viin  4028  iinrabm  4031  2iunin  4035  riin0  4040  iunxprg  4049  unopab  4166  cbvmptf  4181  cbvmpt  4182  exmid1stab  4296  unisucg  4509  op1stb  4573  orddif  4643  elxpi  4739  csbxpg  4805  relopabi  4853  inxp  4862  coeq12i  4891  dfdm3  4915  dfrn3  4917  dmun  4936  dmopab  4940  dmopab3  4942  dmxpid  4951  dmxpin  4952  rnopab  4977  rnmpt  4978  rncoss  5001  rncoeq  5004  reseq12i  5009  resundi  5024  resindi  5026  resiun1  5030  resdmdfsn  5054  resopab  5055  opabresid  5064  dfima3  5077  mptima  5086  imadisj  5096  ndmima  5111  mptcnv  5137  rnun  5143  rnuni  5146  imaundi  5147  inimass  5151  cnvxp  5153  rnxpm  5164  dminxp  5179  imainrect  5180  cnvcnv3  5184  dmpropg  5207  op1sta  5216  op2ndb  5218  op2nda  5219  resdmres  5226  mptpreima  5228  coundi  5236  coundir  5237  cocnvcnv1  5245  cores2  5247  dfdm2  5269  iotajust  5283  dfiota2  5285  funi  5356  funtp  5380  fntpg  5383  funcnvuni  5396  funcnvres  5400  imadiflem  5406  imadif  5407  imainlem  5408  imain  5409  fnresdisj  5439  mptfng  5455  resdif  5602  fv2  5630  dffv4g  5632  fveq12i  5641  nfvres  5671  0fv  5673  dfimafn2  5691  fnimapr  5702  fvmptss2  5717  fvmptg  5718  fvmpts  5720  fvmpt2  5726  mptfvex  5728  elfvmptrab  5738  fvopab6  5739  f1ompt  5794  dfmpt  5820  ressnop0  5830  fprg  5832  fvsnun1  5846  fsnunfv  5850  fvpr2g  5856  imauni  5897  fliftfuns  5934  cbvriota  5978  oveq123i  6027  fconstmpo  6111  resoprab  6112  mpofun  6118  rnmpo  6127  reldmmpo  6128  ov  6136  ovigg  6137  ovmpt4g  6139  ovg  6156  caov31  6207  elmpocl  6212  f1ocnvd  6220  oprabrexex2  6287  op1st  6304  op2nd  6305  f1stres  6317  f2ndres  6318  unielxp  6332  dfoprab3s  6348  dfoprab4  6350  mpompts  6358  mpofvex  6365  oprab2co  6378  df1st2  6379  df2nd2  6380  f1od2  6395  elmpom  6398  brtpos0  6413  tposoprab  6441  smores3  6454  tfrlemi14d  6494  tfr1onlemaccex  6509  tfrcllemaccex  6522  rdgisuc1  6545  rdg0  6548  frec0g  6558  df1o2  6591  df2o2  6593  oasuc  6627  omv2  6628  omsuc  6635  ecidsn  6746  qliftfuns  6783  oviec  6805  mapsncnv  6859  dfixp  6864  xpcomco  7005  xpassen  7009  ssenen  7032  undifdc  7111  unfiin  7113  fidcenumlemrks  7146  fidcenumlemr  7148  sbthlemi5  7154  sbthlemi8  7157  fi0  7168  inf00  7224  djuf1olemr  7247  djuinr  7256  djuin  7257  djuun  7260  casefun  7278  casedm  7279  caseinj  7282  caseinl  7284  caseinr  7285  endjusym  7289  eninl  7290  eninr  7291  djudm  7298  djuinj  7299  fodjuomni  7342  fodjumkv  7353  nninfwlporlemd  7365  pm54.43  7389  exmidfodomrlemim  7405  xp2dju  7423  djucomen  7424  djuassen  7425  xpdjuen  7426  pw1nel3  7442  sucpw1nel3  7444  addpiord  7529  mulpiord  7530  dmaddpi  7538  dmmulpi  7539  recmulnqg  7604  1lt2nq  7619  halfnqq  7623  dfmq0qs  7642  dfplq0qs  7643  genpdf  7721  1prl  7768  1pru  7769  ltexprlemell  7811  ltexprlemelu  7812  recexprlemell  7835  recexprlemelu  7836  cauappcvgprlemm  7858  cauappcvgprlemopl  7859  cauappcvgprlemlol  7860  cauappcvgprlemopu  7861  cauappcvgprlemupu  7862  cauappcvgprlemdisj  7864  cauappcvgprlemloc  7865  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  cauappcvgprlemladdrl  7870  cauappcvgprlem2  7873  caucvgprlemm  7881  caucvgprlemopl  7882  caucvgprlemlol  7883  caucvgprlemopu  7884  caucvgprlemupu  7885  caucvgprlemdisj  7887  caucvgprlemloc  7888  caucvgprlemcl  7889  caucvgprlemladdfu  7890  caucvgprlemladdrl  7891  caucvgprlem2  7893  caucvgprprlemell  7898  caucvgprprlemelu  7899  caucvgprprlemml  7907  caucvgprprlemmu  7908  caucvgprprlemclphr  7918  caucvgprprlemexbt  7919  caucvgprprlem2  7923  addsrpr  7958  mulsrpr  7959  caucvgsrlemoffres  8013  caucvgsr  8015  suplocsrlempr  8020  addcnsr  8047  mulcnsr  8048  mulresr  8051  addvalex  8057  pitonnlem1  8058  axi2m1  8088  axcnre  8094  mulcomli  8179  mnfnre  8215  addcomli  8317  add42i  8338  mvrraddi  8389  neg0  8418  negdii  8456  negsubdi2i  8458  crap0  9131  2t2e4  9291  3t2e6  9293  3t3e9  9294  4t2e8  9295  neg1mulneg1e1  9349  8th4div3  9356  halfpm6th  9357  iap0  9360  dfdec10  9607  deceq12i  9612  numltc  9629  decsuc  9634  decsucc  9644  nummac  9648  numma2c  9649  numadd  9650  numaddc  9651  nummul1c  9652  nummul2c  9653  decma  9654  decmac  9655  decma2c  9656  decadd  9657  decaddc  9658  decrmanc  9660  decrmac  9661  decaddci  9664  decsubi  9666  decmul1  9667  decmul1c  9668  decmul2c  9669  11multnc  9671  4t3lem  9700  6t2e12  9707  7t2e14  9712  8t2e16  9718  9t2e18  9725  9t11e99  9733  halfthird  9746  5recm6rec  9747  divfnzn  9848  xnegpnf  10056  xneg0  10059  xaddmnf1  10076  xaddmnf2  10077  mnfaddpnf  10079  iooval2  10143  dfioo2  10202  fzval2  10239  fzsuc2  10307  fztpval  10311  fz0to3un2pr  10351  fz0to4untppr  10352  fzo01  10454  fzo12sn  10455  fzo0to42pr  10458  fldiv4p1lem1div2  10558  intqfrac2  10574  intfracq  10575  xnn0nnen  10692  1tonninf  10696  neg1sqe1  10889  sq2  10890  sq3  10891  cu2  10893  i2  10895  i3  10896  binom2i  10903  sq10  10967  3dec  10969  facp1  10985  fac2  10986  fac4  10988  4bc2eq6  11029  hashp1i  11067  pr0hash2ex  11072  hashfzo  11079  hashxp  11083  zfz1isolem1  11097  elovmpowrd  11148  ccat1st1st  11211  cji  11456  cnrecnv  11464  sqrt0  11558  resqrexlemover  11564  resqrexlemcalc3  11570  absi  11613  absimle  11638  sumeq12i  11919  summodclem2a  11935  summodc  11937  sum0  11942  fsumsplitf  11962  fsum2dlemstep  11988  fsumabs  12019  fsumiun  12031  0.999...  12075  mertenslem2  12090  prodeq12i  12117  prodmodc  12132  fprod2dlemstep  12176  ege2le3  12225  eft0val  12247  cos0  12284  cos1bnd  12313  cos2bnd  12314  3dvdsdec  12419  3dvds2dec  12420  odd2np1  12427  opoe  12449  nn0o  12461  5ndvds3  12488  5ndvds6  12489  bitsfzolem  12508  m1bits  12514  gcd0val  12524  6gcd4e2  12559  nnmindc  12598  nnminle  12599  3lcm2e6woprm  12651  3lcm2e6  12725  nn0gcdsq  12765  phiprmpw  12787  phimullem  12790  pcprecl  12855  pcprendvds  12856  pcmptdvds  12911  pockthi  12924  4sqlem13m  12969  4sqlem14  12970  4sqlem17  12973  4sqlem18  12974  4sqlem19  12975  dec5nprm  12980  dec2nprm  12981  modxai  12982  modsubi  12985  numexp2x  12991  decsplit0b  12992  decsplit0  12993  decsplit  12995  karatsuba  12996  2exp5  12998  2exp7  13000  2exp8  13001  2exp11  13002  2exp16  13003  3exp3  13004  unennn  13011  ennnfonelemj0  13015  ennnfonelem0  13019  ennnfonelem1  13021  ennnfonelemhf1o  13027  ennnfonelemrn  13033  ennnfonelemdm  13034  strnfvnd  13095  slotslfn  13101  setsfun  13110  setsfun0  13111  setscom  13115  setsslid  13126  2strstr1g  13198  eqglact  13805  ecqusaddd  13818  ghmeqker  13851  dfrhm2  14161  rmodislmod  14358  cnfldadd  14569  cnfldmul  14571  expghmap  14614  fczpsrbag  14678  cnco  14938  txuni2  14973  txbas  14975  uptx  14991  txcn  14992  cnmptid  14998  cnmpt2t  15010  xmetxp  15224  cnmetdval  15246  remetdval  15264  resubmet  15273  rerestcntop  15275  rerest  15277  divcnap  15282  cnrehmeocntop  15327  dvexp  15428  plyun0  15453  plyco  15476  plycj  15478  sinhalfpilem  15508  cosneghalfpi  15515  efhalfpi  15516  cospi  15517  efipi  15518  eulerid  15519  sin2pi  15520  cos2pi  15521  ef2pi  15522  sincosq4sgn  15546  cosq14gt0  15549  tangtx  15555  sincos4thpi  15557  sincos6thpi  15559  sinkpi  15564  cosq34lt1  15567  dfrelog  15577  2logb9irr  15688  2logb9irrALT  15691  2logb9irrap  15694  mersenne  15714  perfectlem2  15717  zabsle1  15721  lgslem2  15723  lgsfcl2  15728  lgsdir2lem1  15750  lgsdir2lem2  15751  lgsdir2lem4  15753  lgsdir2lem5  15754  lgseisen  15796  2lgslem3a  15815  2lgslem3b  15816  2lgslem3c  15817  2lgslem3d  15818  2lgs2  15824  2lgsoddprmlem3a  15829  2lgsoddprmlem3b  15830  2lgsoddprmlem3c  15831  2lgsoddprmlem3d  15832  pw0ss  15927  umgrislfupgrenlem  15974  vtxdgfval  16099  clwwlknon2  16243  clwwlknon2x  16244  ex-fl  16271  ex-exp  16273  ex-fac  16274  ex-bc  16275  ex-dvds  16276  ex-gcd  16277  bj-dfom  16478  012of  16542  2o01f  16543  pwle2  16549  nninfsellemqall  16567  isomninnlem  16584  iswomninnlem  16603  ismkvnnlem  16606  dceqnconst  16614  dcapnconst  16615  taupi  16627