Theorem eqtri 2252

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

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtr2i  2253  eqtr3i  2254  eqtr4i  2255  3eqtri  2256  3eqtrri  2257  3eqtr2i  2258  cbvrab  2800  csb2  3129  cbvrabcsf  3193  difjust  3201  unjust  3203  injust  3205  dfdif3  3317  difeq12i  3323  inrot  3422  symdif1  3472  rabnc  3527  0in  3530  ssdifin0  3576  dfif3  3619  ifbieq2i  3629  ifbieq12i  3631  pwjust  3653  snjust  3674  dfpr2  3688  disjpr2  3733  rabsnifsb  3737  difprsn1  3812  diftpsn3  3814  difpr  3815  dfuni2  3895  intab  3957  intunsn  3966  rint0  3967  iunid  4026  viin  4030  iinrabm  4033  2iunin  4037  riin0  4042  iunxprg  4051  unopab  4168  cbvmptf  4183  cbvmpt  4184  exmid1stab  4298  unisucg  4511  op1stb  4575  orddif  4645  elxpi  4741  csbxpg  4807  relopabi  4855  inxp  4864  coeq12i  4893  dfdm3  4917  dfrn3  4919  dmun  4938  dmopab  4942  dmopab3  4944  dmxpid  4953  dmxpin  4954  rnopab  4979  rnmpt  4980  rncoss  5003  rncoeq  5006  reseq12i  5011  resundi  5026  resindi  5028  resiun1  5032  resdmdfsn  5056  resopab  5057  opabresid  5066  dfima3  5079  mptima  5088  imadisj  5098  ndmima  5113  mptcnv  5139  rnun  5145  rnuni  5148  imaundi  5149  inimass  5153  cnvxp  5155  rnxpm  5166  dminxp  5181  imainrect  5182  cnvcnv3  5186  dmpropg  5209  op1sta  5218  op2ndb  5220  op2nda  5221  resdmres  5228  mptpreima  5230  coundi  5238  coundir  5239  cocnvcnv1  5247  cores2  5249  dfdm2  5271  iotajust  5285  dfiota2  5287  funi  5358  funtp  5383  fntpg  5386  funcnvuni  5399  funcnvres  5403  imadiflem  5409  imadif  5410  imainlem  5411  imain  5412  fnresdisj  5442  mptfng  5458  resdif  5605  fv2  5634  dffv4g  5636  fveq12i  5645  nfvres  5675  0fv  5677  dfimafn2  5695  fnimapr  5706  fvmptss2  5721  fvmptg  5722  fvmpts  5724  fvmpt2  5730  mptfvex  5732  elfvmptrab  5742  fvopab6  5743  f1ompt  5798  dfmpt  5825  ressnop0  5835  fprg  5837  fvsnun1  5851  fsnunfv  5855  fvpr2g  5861  imauni  5902  fliftfuns  5939  cbvriota  5983  oveq123i  6032  fconstmpo  6116  resoprab  6117  mpofun  6123  rnmpo  6132  reldmmpo  6133  ov  6141  ovigg  6142  ovmpt4g  6144  ovg  6161  caov31  6212  elmpocl  6217  f1ocnvd  6225  oprabrexex2  6292  op1st  6309  op2nd  6310  f1stres  6322  f2ndres  6323  unielxp  6337  dfoprab3s  6353  dfoprab4  6355  mpompts  6363  mpofvex  6370  oprab2co  6383  df1st2  6384  df2nd2  6385  f1od2  6400  elmpom  6403  brtpos0  6418  tposoprab  6446  smores3  6459  tfrlemi14d  6499  tfr1onlemaccex  6514  tfrcllemaccex  6527  rdgisuc1  6550  rdg0  6553  frec0g  6563  df1o2  6596  df2o2  6598  oasuc  6632  omv2  6633  omsuc  6640  ecidsn  6751  qliftfuns  6788  oviec  6810  mapsncnv  6864  dfixp  6869  xpcomco  7010  xpassen  7014  ssenen  7037  undifdc  7116  unfiin  7118  fidcenumlemrks  7152  fidcenumlemr  7154  sbthlemi5  7160  sbthlemi8  7163  fi0  7174  inf00  7230  djuf1olemr  7253  djuinr  7262  djuin  7263  djuun  7266  casefun  7284  casedm  7285  caseinj  7288  caseinl  7290  caseinr  7291  endjusym  7295  eninl  7296  eninr  7297  djudm  7304  djuinj  7305  fodjuomni  7348  fodjumkv  7359  nninfwlporlemd  7371  pm54.43  7395  exmidfodomrlemim  7412  xp2dju  7430  djucomen  7431  djuassen  7432  xpdjuen  7433  pw1nel3  7449  sucpw1nel3  7451  addpiord  7536  mulpiord  7537  dmaddpi  7545  dmmulpi  7546  recmulnqg  7611  1lt2nq  7626  halfnqq  7630  dfmq0qs  7649  dfplq0qs  7650  genpdf  7728  1prl  7775  1pru  7776  ltexprlemell  7818  ltexprlemelu  7819  recexprlemell  7842  recexprlemelu  7843  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem2  7900  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem2  7930  addsrpr  7965  mulsrpr  7966  caucvgsrlemoffres  8020  caucvgsr  8022  suplocsrlempr  8027  addcnsr  8054  mulcnsr  8055  mulresr  8058  addvalex  8064  pitonnlem1  8065  axi2m1  8095  axcnre  8101  mulcomli  8186  mnfnre  8222  addcomli  8324  add42i  8345  mvrraddi  8396  neg0  8425  negdii  8463  negsubdi2i  8465  crap0  9138  2t2e4  9298  3t2e6  9300  3t3e9  9301  4t2e8  9302  neg1mulneg1e1  9356  8th4div3  9363  halfpm6th  9364  iap0  9367  dfdec10  9614  deceq12i  9619  numltc  9636  decsuc  9641  decsucc  9651  nummac  9655  numma2c  9656  numadd  9657  numaddc  9658  nummul1c  9659  nummul2c  9660  decma  9661  decmac  9662  decma2c  9663  decadd  9664  decaddc  9665  decrmanc  9667  decrmac  9668  decaddci  9671  decsubi  9673  decmul1  9674  decmul1c  9675  decmul2c  9676  11multnc  9678  4t3lem  9707  6t2e12  9714  7t2e14  9719  8t2e16  9725  9t2e18  9732  9t11e99  9740  halfthird  9753  5recm6rec  9754  divfnzn  9855  xnegpnf  10063  xneg0  10066  xaddmnf1  10083  xaddmnf2  10084  mnfaddpnf  10086  iooval2  10150  dfioo2  10209  fzval2  10246  fzsuc2  10314  fztpval  10318  fz0to3un2pr  10358  fz0to4untppr  10359  fzo01  10462  fzo12sn  10463  fzo0to42pr  10466  fldiv4p1lem1div2  10566  intqfrac2  10582  intfracq  10583  xnn0nnen  10700  1tonninf  10704  neg1sqe1  10897  sq2  10898  sq3  10899  cu2  10901  i2  10903  i3  10904  binom2i  10911  sq10  10975  3dec  10977  facp1  10993  fac2  10994  fac4  10996  4bc2eq6  11037  hashp1i  11075  pr0hash2ex  11080  hashfzo  11087  hashxp  11091  zfz1isolem1  11105  elovmpowrd  11159  ccat1st1st  11222  cji  11467  cnrecnv  11475  sqrt0  11569  resqrexlemover  11575  resqrexlemcalc3  11581  absi  11624  absimle  11649  sumeq12i  11930  summodclem2a  11947  summodc  11949  sum0  11954  fsumsplitf  11974  fsum2dlemstep  12000  fsumabs  12031  fsumiun  12043  0.999...  12087  mertenslem2  12102  prodeq12i  12129  prodmodc  12144  fprod2dlemstep  12188  ege2le3  12237  eft0val  12259  cos0  12296  cos1bnd  12325  cos2bnd  12326  3dvdsdec  12431  3dvds2dec  12432  odd2np1  12439  opoe  12461  nn0o  12473  5ndvds3  12500  5ndvds6  12501  bitsfzolem  12520  m1bits  12526  gcd0val  12536  6gcd4e2  12571  nnmindc  12610  nnminle  12611  3lcm2e6woprm  12663  3lcm2e6  12737  nn0gcdsq  12777  phiprmpw  12799  phimullem  12802  pcprecl  12867  pcprendvds  12868  pcmptdvds  12923  pockthi  12936  4sqlem13m  12981  4sqlem14  12982  4sqlem17  12985  4sqlem18  12986  4sqlem19  12987  dec5nprm  12992  dec2nprm  12993  modxai  12994  modsubi  12997  numexp2x  13003  decsplit0b  13004  decsplit0  13005  decsplit  13007  karatsuba  13008  2exp5  13010  2exp7  13012  2exp8  13013  2exp11  13014  2exp16  13015  3exp3  13016  unennn  13023  ennnfonelemj0  13027  ennnfonelem0  13031  ennnfonelem1  13033  ennnfonelemhf1o  13039  ennnfonelemrn  13045  ennnfonelemdm  13046  strnfvnd  13107  slotslfn  13113  setsfun  13122  setsfun0  13123  setscom  13127  setsslid  13138  2strstr1g  13210  eqglact  13817  ecqusaddd  13830  ghmeqker  13863  dfrhm2  14174  rmodislmod  14371  cnfldadd  14582  cnfldmul  14584  expghmap  14627  fczpsrbag  14691  cnco  14951  txuni2  14986  txbas  14988  uptx  15004  txcn  15005  cnmptid  15011  cnmpt2t  15023  xmetxp  15237  cnmetdval  15259  remetdval  15277  resubmet  15286  rerestcntop  15288  rerest  15290  divcnap  15295  cnrehmeocntop  15340  dvexp  15441  plyun0  15466  plyco  15489  plycj  15491  sinhalfpilem  15521  cosneghalfpi  15528  efhalfpi  15529  cospi  15530  efipi  15531  eulerid  15532  sin2pi  15533  cos2pi  15534  ef2pi  15535  sincosq4sgn  15559  cosq14gt0  15562  tangtx  15568  sincos4thpi  15570  sincos6thpi  15572  sinkpi  15577  cosq34lt1  15580  dfrelog  15590  2logb9irr  15701  2logb9irrALT  15704  2logb9irrap  15707  mersenne  15727  perfectlem2  15730  zabsle1  15734  lgslem2  15736  lgsfcl2  15741  lgsdir2lem1  15763  lgsdir2lem2  15764  lgsdir2lem4  15766  lgsdir2lem5  15767  lgseisen  15809  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2lgs2  15837  2lgsoddprmlem3a  15842  2lgsoddprmlem3b  15843  2lgsoddprmlem3c  15844  2lgsoddprmlem3d  15845  pw0ss  15940  umgrislfupgrenlem  15987  vtxdgfval  16145  clwwlknon2  16291  clwwlknon2x  16292  eupth2lembfi  16334  ex-fl  16343  ex-exp  16345  ex-fac  16346  ex-bc  16347  ex-dvds  16348  ex-gcd  16349  bj-dfom  16554  012of  16618  2o01f  16619  pwle2  16625  nninfsellemqall  16643  isomninnlem  16660  iswomninnlem  16679  ismkvnnlem  16682  dceqnconst  16690  dcapnconst  16691  taupi  16703  gfsump1  16712