Theorem eqtri 2227

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

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqtr2i  2228  eqtr3i  2229  eqtr4i  2230  3eqtri  2231  3eqtrri  2232  3eqtr2i  2233  cbvrab  2771  csb2  3097  cbvrabcsf  3161  difjust  3169  unjust  3171  injust  3173  dfdif3  3285  difeq12i  3291  inrot  3390  symdif1  3440  rabnc  3495  0in  3498  ssdifin0  3544  dfif3  3586  ifbieq2i  3596  ifbieq12i  3598  pwjust  3619  snjust  3640  dfpr2  3654  disjpr2  3699  difprsn1  3775  diftpsn3  3777  difpr  3778  dfuni2  3855  intab  3917  intunsn  3926  rint0  3927  iunid  3986  viin  3990  iinrabm  3993  2iunin  3997  riin0  4002  iunxprg  4011  unopab  4128  cbvmptf  4143  cbvmpt  4144  exmid1stab  4257  unisucg  4466  op1stb  4530  orddif  4600  elxpi  4696  csbxpg  4761  relopabi  4808  inxp  4817  coeq12i  4846  dfdm3  4870  dfrn3  4872  dmun  4891  dmopab  4895  dmopab3  4897  dmxpid  4905  dmxpin  4906  rnopab  4931  rnmpt  4932  rncoss  4955  rncoeq  4958  reseq12i  4963  resundi  4978  resindi  4980  resiun1  4984  resdmdfsn  5008  resopab  5009  opabresid  5018  dfima3  5031  mptima  5040  imadisj  5050  ndmima  5065  mptcnv  5091  rnun  5097  rnuni  5100  imaundi  5101  inimass  5105  cnvxp  5107  rnxpm  5118  dminxp  5133  imainrect  5134  cnvcnv3  5138  dmpropg  5161  op1sta  5170  op2ndb  5172  op2nda  5173  resdmres  5180  mptpreima  5182  coundi  5190  coundir  5191  cocnvcnv1  5199  cores2  5201  dfdm2  5223  iotajust  5237  dfiota2  5239  funi  5309  funtp  5333  fntpg  5336  funcnvuni  5349  funcnvres  5353  imadiflem  5359  imadif  5360  imainlem  5361  imain  5362  fnresdisj  5392  mptfng  5408  resdif  5553  fv2  5581  dffv4g  5583  fveq12i  5592  nfvres  5620  0fv  5622  dfimafn2  5638  fnimapr  5649  fvmptss2  5664  fvmptg  5665  fvmpts  5667  fvmpt2  5673  mptfvex  5675  elfvmptrab  5685  fvopab6  5686  f1ompt  5741  dfmpt  5767  ressnop0  5775  fprg  5777  fvsnun1  5791  fsnunfv  5795  fvpr2g  5801  imauni  5840  fliftfuns  5877  cbvriota  5920  oveq123i  5968  fconstmpo  6050  resoprab  6051  mpofun  6057  rnmpo  6066  reldmmpo  6067  ov  6075  ovigg  6076  ovmpt4g  6078  ovg  6095  caov31  6146  elmpocl  6151  f1ocnvd  6158  oprabrexex2  6225  op1st  6242  op2nd  6243  f1stres  6255  f2ndres  6256  unielxp  6270  dfoprab3s  6286  dfoprab4  6288  mpompts  6294  mpofvex  6301  oprab2co  6314  df1st2  6315  df2nd2  6316  f1od2  6331  brtpos0  6348  tposoprab  6376  smores3  6389  tfrlemi14d  6429  tfr1onlemaccex  6444  tfrcllemaccex  6457  rdgisuc1  6480  rdg0  6483  frec0g  6493  df1o2  6525  df2o2  6527  oasuc  6560  omv2  6561  omsuc  6568  ecidsn  6679  qliftfuns  6716  oviec  6738  mapsncnv  6792  dfixp  6797  xpcomco  6933  xpassen  6937  ssenen  6960  undifdc  7033  unfiin  7035  fidcenumlemrks  7067  fidcenumlemr  7069  sbthlemi5  7075  sbthlemi8  7078  fi0  7089  inf00  7145  djuf1olemr  7168  djuinr  7177  djuin  7178  djuun  7181  casefun  7199  casedm  7200  caseinj  7203  caseinl  7205  caseinr  7206  endjusym  7210  eninl  7211  eninr  7212  djudm  7219  djuinj  7220  fodjuomni  7263  fodjumkv  7274  nninfwlporlemd  7286  pm54.43  7310  exmidfodomrlemim  7322  xp2dju  7340  djucomen  7341  djuassen  7342  xpdjuen  7343  pw1nel3  7356  sucpw1nel3  7358  addpiord  7442  mulpiord  7443  dmaddpi  7451  dmmulpi  7452  recmulnqg  7517  1lt2nq  7532  halfnqq  7536  dfmq0qs  7555  dfplq0qs  7556  genpdf  7634  1prl  7681  1pru  7682  ltexprlemell  7724  ltexprlemelu  7725  recexprlemell  7748  recexprlemelu  7749  cauappcvgprlemm  7771  cauappcvgprlemopl  7772  cauappcvgprlemlol  7773  cauappcvgprlemopu  7774  cauappcvgprlemupu  7775  cauappcvgprlemdisj  7777  cauappcvgprlemloc  7778  cauappcvgprlemladdfu  7780  cauappcvgprlemladdfl  7781  cauappcvgprlemladdrl  7783  cauappcvgprlem2  7786  caucvgprlemm  7794  caucvgprlemopl  7795  caucvgprlemlol  7796  caucvgprlemopu  7797  caucvgprlemupu  7798  caucvgprlemdisj  7800  caucvgprlemloc  7801  caucvgprlemcl  7802  caucvgprlemladdfu  7803  caucvgprlemladdrl  7804  caucvgprlem2  7806  caucvgprprlemell  7811  caucvgprprlemelu  7812  caucvgprprlemml  7820  caucvgprprlemmu  7821  caucvgprprlemclphr  7831  caucvgprprlemexbt  7832  caucvgprprlem2  7836  addsrpr  7871  mulsrpr  7872  caucvgsrlemoffres  7926  caucvgsr  7928  suplocsrlempr  7933  addcnsr  7960  mulcnsr  7961  mulresr  7964  addvalex  7970  pitonnlem1  7971  axi2m1  8001  axcnre  8007  mulcomli  8092  mnfnre  8128  addcomli  8230  add42i  8251  mvrraddi  8302  neg0  8331  negdii  8369  negsubdi2i  8371  crap0  9044  2t2e4  9204  3t2e6  9206  3t3e9  9207  4t2e8  9208  neg1mulneg1e1  9262  8th4div3  9269  halfpm6th  9270  iap0  9273  dfdec10  9520  deceq12i  9525  numltc  9542  decsuc  9547  decsucc  9557  nummac  9561  numma2c  9562  numadd  9563  numaddc  9564  nummul1c  9565  nummul2c  9566  decma  9567  decmac  9568  decma2c  9569  decadd  9570  decaddc  9571  decrmanc  9573  decrmac  9574  decaddci  9577  decsubi  9579  decmul1  9580  decmul1c  9581  decmul2c  9582  11multnc  9584  4t3lem  9613  6t2e12  9620  7t2e14  9625  8t2e16  9631  9t2e18  9638  9t11e99  9646  halfthird  9659  5recm6rec  9660  divfnzn  9755  xnegpnf  9963  xneg0  9966  xaddmnf1  9983  xaddmnf2  9984  mnfaddpnf  9986  iooval2  10050  dfioo2  10109  fzval2  10146  fzsuc2  10214  fztpval  10218  fz0to3un2pr  10258  fz0to4untppr  10259  fzo01  10358  fzo12sn  10359  fzo0to42pr  10362  fldiv4p1lem1div2  10461  intqfrac2  10477  intfracq  10478  xnn0nnen  10595  1tonninf  10599  neg1sqe1  10792  sq2  10793  sq3  10794  cu2  10796  i2  10798  i3  10799  binom2i  10806  sq10  10870  3dec  10872  facp1  10888  fac2  10889  fac4  10891  4bc2eq6  10932  hashp1i  10968  pr0hash2ex  10973  hashfzo  10980  hashxp  10984  zfz1isolem1  10998  elovmpowrd  11048  ccat1st1st  11107  cji  11263  cnrecnv  11271  sqrt0  11365  resqrexlemover  11371  resqrexlemcalc3  11377  absi  11420  absimle  11445  sumeq12i  11726  summodclem2a  11742  summodc  11744  sum0  11749  fsumsplitf  11769  fsum2dlemstep  11795  fsumabs  11826  fsumiun  11838  0.999...  11882  mertenslem2  11897  prodeq12i  11924  prodmodc  11939  fprod2dlemstep  11983  ege2le3  12032  eft0val  12054  cos0  12091  cos1bnd  12120  cos2bnd  12121  3dvdsdec  12226  3dvds2dec  12227  odd2np1  12234  opoe  12256  nn0o  12268  5ndvds3  12295  5ndvds6  12296  bitsfzolem  12315  m1bits  12321  gcd0val  12331  6gcd4e2  12366  nnmindc  12405  nnminle  12406  3lcm2e6woprm  12458  3lcm2e6  12532  nn0gcdsq  12572  phiprmpw  12594  phimullem  12597  pcprecl  12662  pcprendvds  12663  pcmptdvds  12718  pockthi  12731  4sqlem13m  12776  4sqlem14  12777  4sqlem17  12780  4sqlem18  12781  4sqlem19  12782  dec5nprm  12787  dec2nprm  12788  modxai  12789  modsubi  12792  numexp2x  12798  decsplit0b  12799  decsplit0  12800  decsplit  12802  karatsuba  12803  2exp5  12805  2exp7  12807  2exp8  12808  2exp11  12809  2exp16  12810  3exp3  12811  unennn  12818  ennnfonelemj0  12822  ennnfonelem0  12826  ennnfonelem1  12828  ennnfonelemhf1o  12834  ennnfonelemrn  12840  ennnfonelemdm  12841  strnfvnd  12902  slotslfn  12908  setsfun  12917  setsfun0  12918  setscom  12922  setsslid  12933  2strstr1g  13004  eqglact  13611  ecqusaddd  13624  ghmeqker  13657  dfrhm2  13966  rmodislmod  14163  cnfldadd  14374  cnfldmul  14376  expghmap  14419  fczpsrbag  14483  cnco  14743  txuni2  14778  txbas  14780  uptx  14796  txcn  14797  cnmptid  14803  cnmpt2t  14815  xmetxp  15029  cnmetdval  15051  remetdval  15069  resubmet  15078  rerestcntop  15080  rerest  15082  divcnap  15087  cnrehmeocntop  15132  dvexp  15233  plyun0  15258  plyco  15281  plycj  15283  sinhalfpilem  15313  cosneghalfpi  15320  efhalfpi  15321  cospi  15322  efipi  15323  eulerid  15324  sin2pi  15325  cos2pi  15326  ef2pi  15327  sincosq4sgn  15351  cosq14gt0  15354  tangtx  15360  sincos4thpi  15362  sincos6thpi  15364  sinkpi  15369  cosq34lt1  15372  dfrelog  15382  2logb9irr  15493  2logb9irrALT  15496  2logb9irrap  15499  mersenne  15519  perfectlem2  15522  zabsle1  15526  lgslem2  15528  lgsfcl2  15533  lgsdir2lem1  15555  lgsdir2lem2  15556  lgsdir2lem4  15558  lgsdir2lem5  15559  lgseisen  15601  2lgslem3a  15620  2lgslem3b  15621  2lgslem3c  15622  2lgslem3d  15623  2lgs2  15629  2lgsoddprmlem3a  15634  2lgsoddprmlem3b  15635  2lgsoddprmlem3c  15636  2lgsoddprmlem3d  15637  pw0ss  15729  ex-fl  15775  ex-exp  15777  ex-fac  15778  ex-bc  15779  ex-dvds  15780  ex-gcd  15781  bj-dfom  15983  012of  16045  2o01f  16046  pwle2  16050  nninfsellemqall  16067  isomninnlem  16084  iswomninnlem  16103  ismkvnnlem  16106  dceqnconst  16114  dcapnconst  16115  taupi  16127