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  2797  csb2  3126  cbvrabcsf  3190  difjust  3198  unjust  3200  injust  3202  dfdif3  3314  difeq12i  3320  inrot  3419  symdif1  3469  rabnc  3524  0in  3527  ssdifin0  3573  dfif3  3616  ifbieq2i  3626  ifbieq12i  3628  pwjust  3650  snjust  3671  dfpr2  3685  disjpr2  3730  difprsn1  3807  diftpsn3  3809  difpr  3810  dfuni2  3890  intab  3952  intunsn  3961  rint0  3962  iunid  4021  viin  4025  iinrabm  4028  2iunin  4032  riin0  4037  iunxprg  4046  unopab  4163  cbvmptf  4178  cbvmpt  4179  exmid1stab  4293  unisucg  4506  op1stb  4570  orddif  4640  elxpi  4736  csbxpg  4802  relopabi  4850  inxp  4859  coeq12i  4888  dfdm3  4912  dfrn3  4914  dmun  4933  dmopab  4937  dmopab3  4939  dmxpid  4948  dmxpin  4949  rnopab  4974  rnmpt  4975  rncoss  4998  rncoeq  5001  reseq12i  5006  resundi  5021  resindi  5023  resiun1  5027  resdmdfsn  5051  resopab  5052  opabresid  5061  dfima3  5074  mptima  5083  imadisj  5093  ndmima  5108  mptcnv  5134  rnun  5140  rnuni  5143  imaundi  5144  inimass  5148  cnvxp  5150  rnxpm  5161  dminxp  5176  imainrect  5177  cnvcnv3  5181  dmpropg  5204  op1sta  5213  op2ndb  5215  op2nda  5216  resdmres  5223  mptpreima  5225  coundi  5233  coundir  5234  cocnvcnv1  5242  cores2  5244  dfdm2  5266  iotajust  5280  dfiota2  5282  funi  5353  funtp  5377  fntpg  5380  funcnvuni  5393  funcnvres  5397  imadiflem  5403  imadif  5404  imainlem  5405  imain  5406  fnresdisj  5436  mptfng  5452  resdif  5599  fv2  5627  dffv4g  5629  fveq12i  5638  nfvres  5668  0fv  5670  dfimafn2  5688  fnimapr  5699  fvmptss2  5714  fvmptg  5715  fvmpts  5717  fvmpt2  5723  mptfvex  5725  elfvmptrab  5735  fvopab6  5736  f1ompt  5791  dfmpt  5817  ressnop0  5827  fprg  5829  fvsnun1  5843  fsnunfv  5847  fvpr2g  5853  imauni  5894  fliftfuns  5931  cbvriota  5975  oveq123i  6024  fconstmpo  6108  resoprab  6109  mpofun  6115  rnmpo  6124  reldmmpo  6125  ov  6133  ovigg  6134  ovmpt4g  6136  ovg  6153  caov31  6204  elmpocl  6209  f1ocnvd  6217  oprabrexex2  6284  op1st  6301  op2nd  6302  f1stres  6314  f2ndres  6315  unielxp  6329  dfoprab3s  6345  dfoprab4  6347  mpompts  6355  mpofvex  6362  oprab2co  6375  df1st2  6376  df2nd2  6377  f1od2  6392  brtpos0  6409  tposoprab  6437  smores3  6450  tfrlemi14d  6490  tfr1onlemaccex  6505  tfrcllemaccex  6518  rdgisuc1  6541  rdg0  6544  frec0g  6554  df1o2  6587  df2o2  6589  oasuc  6623  omv2  6624  omsuc  6631  ecidsn  6742  qliftfuns  6779  oviec  6801  mapsncnv  6855  dfixp  6860  xpcomco  6998  xpassen  7002  ssenen  7025  undifdc  7102  unfiin  7104  fidcenumlemrks  7136  fidcenumlemr  7138  sbthlemi5  7144  sbthlemi8  7147  fi0  7158  inf00  7214  djuf1olemr  7237  djuinr  7246  djuin  7247  djuun  7250  casefun  7268  casedm  7269  caseinj  7272  caseinl  7274  caseinr  7275  endjusym  7279  eninl  7280  eninr  7281  djudm  7288  djuinj  7289  fodjuomni  7332  fodjumkv  7343  nninfwlporlemd  7355  pm54.43  7379  exmidfodomrlemim  7395  xp2dju  7413  djucomen  7414  djuassen  7415  xpdjuen  7416  pw1nel3  7432  sucpw1nel3  7434  addpiord  7519  mulpiord  7520  dmaddpi  7528  dmmulpi  7529  recmulnqg  7594  1lt2nq  7609  halfnqq  7613  dfmq0qs  7632  dfplq0qs  7633  genpdf  7711  1prl  7758  1pru  7759  ltexprlemell  7801  ltexprlemelu  7802  recexprlemell  7825  recexprlemelu  7826  cauappcvgprlemm  7848  cauappcvgprlemopl  7849  cauappcvgprlemlol  7850  cauappcvgprlemopu  7851  cauappcvgprlemupu  7852  cauappcvgprlemdisj  7854  cauappcvgprlemloc  7855  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlemladdrl  7860  cauappcvgprlem2  7863  caucvgprlemm  7871  caucvgprlemopl  7872  caucvgprlemlol  7873  caucvgprlemopu  7874  caucvgprlemupu  7875  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprlemcl  7879  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgprlem2  7883  caucvgprprlemell  7888  caucvgprprlemelu  7889  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemclphr  7908  caucvgprprlemexbt  7909  caucvgprprlem2  7913  addsrpr  7948  mulsrpr  7949  caucvgsrlemoffres  8003  caucvgsr  8005  suplocsrlempr  8010  addcnsr  8037  mulcnsr  8038  mulresr  8041  addvalex  8047  pitonnlem1  8048  axi2m1  8078  axcnre  8084  mulcomli  8169  mnfnre  8205  addcomli  8307  add42i  8328  mvrraddi  8379  neg0  8408  negdii  8446  negsubdi2i  8448  crap0  9121  2t2e4  9281  3t2e6  9283  3t3e9  9284  4t2e8  9285  neg1mulneg1e1  9339  8th4div3  9346  halfpm6th  9347  iap0  9350  dfdec10  9597  deceq12i  9602  numltc  9619  decsuc  9624  decsucc  9634  nummac  9638  numma2c  9639  numadd  9640  numaddc  9641  nummul1c  9642  nummul2c  9643  decma  9644  decmac  9645  decma2c  9646  decadd  9647  decaddc  9648  decrmanc  9650  decrmac  9651  decaddci  9654  decsubi  9656  decmul1  9657  decmul1c  9658  decmul2c  9659  11multnc  9661  4t3lem  9690  6t2e12  9697  7t2e14  9702  8t2e16  9708  9t2e18  9715  9t11e99  9723  halfthird  9736  5recm6rec  9737  divfnzn  9833  xnegpnf  10041  xneg0  10044  xaddmnf1  10061  xaddmnf2  10062  mnfaddpnf  10064  iooval2  10128  dfioo2  10187  fzval2  10224  fzsuc2  10292  fztpval  10296  fz0to3un2pr  10336  fz0to4untppr  10337  fzo01  10439  fzo12sn  10440  fzo0to42pr  10443  fldiv4p1lem1div2  10542  intqfrac2  10558  intfracq  10559  xnn0nnen  10676  1tonninf  10680  neg1sqe1  10873  sq2  10874  sq3  10875  cu2  10877  i2  10879  i3  10880  binom2i  10887  sq10  10951  3dec  10953  facp1  10969  fac2  10970  fac4  10972  4bc2eq6  11013  hashp1i  11050  pr0hash2ex  11055  hashfzo  11062  hashxp  11066  zfz1isolem1  11080  elovmpowrd  11131  ccat1st1st  11193  cji  11434  cnrecnv  11442  sqrt0  11536  resqrexlemover  11542  resqrexlemcalc3  11548  absi  11591  absimle  11616  sumeq12i  11897  summodclem2a  11913  summodc  11915  sum0  11920  fsumsplitf  11940  fsum2dlemstep  11966  fsumabs  11997  fsumiun  12009  0.999...  12053  mertenslem2  12068  prodeq12i  12095  prodmodc  12110  fprod2dlemstep  12154  ege2le3  12203  eft0val  12225  cos0  12262  cos1bnd  12291  cos2bnd  12292  3dvdsdec  12397  3dvds2dec  12398  odd2np1  12405  opoe  12427  nn0o  12439  5ndvds3  12466  5ndvds6  12467  bitsfzolem  12486  m1bits  12492  gcd0val  12502  6gcd4e2  12537  nnmindc  12576  nnminle  12577  3lcm2e6woprm  12629  3lcm2e6  12703  nn0gcdsq  12743  phiprmpw  12765  phimullem  12768  pcprecl  12833  pcprendvds  12834  pcmptdvds  12889  pockthi  12902  4sqlem13m  12947  4sqlem14  12948  4sqlem17  12951  4sqlem18  12952  4sqlem19  12953  dec5nprm  12958  dec2nprm  12959  modxai  12960  modsubi  12963  numexp2x  12969  decsplit0b  12970  decsplit0  12971  decsplit  12973  karatsuba  12974  2exp5  12976  2exp7  12978  2exp8  12979  2exp11  12980  2exp16  12981  3exp3  12982  unennn  12989  ennnfonelemj0  12993  ennnfonelem0  12997  ennnfonelem1  12999  ennnfonelemhf1o  13005  ennnfonelemrn  13011  ennnfonelemdm  13012  strnfvnd  13073  slotslfn  13079  setsfun  13088  setsfun0  13089  setscom  13093  setsslid  13104  2strstr1g  13176  eqglact  13783  ecqusaddd  13796  ghmeqker  13829  dfrhm2  14139  rmodislmod  14336  cnfldadd  14547  cnfldmul  14549  expghmap  14592  fczpsrbag  14656  cnco  14916  txuni2  14951  txbas  14953  uptx  14969  txcn  14970  cnmptid  14976  cnmpt2t  14988  xmetxp  15202  cnmetdval  15224  remetdval  15242  resubmet  15251  rerestcntop  15253  rerest  15255  divcnap  15260  cnrehmeocntop  15305  dvexp  15406  plyun0  15431  plyco  15454  plycj  15456  sinhalfpilem  15486  cosneghalfpi  15493  efhalfpi  15494  cospi  15495  efipi  15496  eulerid  15497  sin2pi  15498  cos2pi  15499  ef2pi  15500  sincosq4sgn  15524  cosq14gt0  15527  tangtx  15533  sincos4thpi  15535  sincos6thpi  15537  sinkpi  15542  cosq34lt1  15545  dfrelog  15555  2logb9irr  15666  2logb9irrALT  15669  2logb9irrap  15672  mersenne  15692  perfectlem2  15695  zabsle1  15699  lgslem2  15701  lgsfcl2  15706  lgsdir2lem1  15728  lgsdir2lem2  15729  lgsdir2lem4  15731  lgsdir2lem5  15732  lgseisen  15774  2lgslem3a  15793  2lgslem3b  15794  2lgslem3c  15795  2lgslem3d  15796  2lgs2  15802  2lgsoddprmlem3a  15807  2lgsoddprmlem3b  15808  2lgsoddprmlem3c  15809  2lgsoddprmlem3d  15810  pw0ss  15904  umgrislfupgrenlem  15949  vtxdgfval  16074  ex-fl  16198  ex-exp  16200  ex-fac  16201  ex-bc  16202  ex-dvds  16203  ex-gcd  16204  bj-dfom  16405  012of  16470  2o01f  16471  pwle2  16477  nninfsellemqall  16495  isomninnlem  16512  iswomninnlem  16531  ismkvnnlem  16534  dceqnconst  16542  dcapnconst  16543  taupi  16555