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  7372  djuf1olemr  7395  djuinr  7404  djuin  7405  djuun  7408  casefun  7426  casedm  7427  caseinj  7430  caseinl  7432  caseinr  7433  endjusym  7437  eninl  7438  eninr  7439  djudm  7446  djuinj  7447  fodjuomni  7490  fodjumkv  7501  nninfwlporlemd  7513  pm54.43  7537  exmidfodomrlemim  7554  xp2dju  7572  djucomen  7573  djuassen  7574  xpdjuen  7575  pw1nel3  7591  sucpw1nel3  7593  addpiord  7684  mulpiord  7685  dmaddpi  7693  dmmulpi  7694  recmulnqg  7759  1lt2nq  7774  halfnqq  7778  dfmq0qs  7797  dfplq0qs  7798  genpdf  7876  1prl  7923  1pru  7924  ltexprlemell  7966  ltexprlemelu  7967  recexprlemell  7990  recexprlemelu  7991  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdrl  8025  cauappcvgprlem2  8028  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem2  8048  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem2  8078  addsrpr  8113  mulsrpr  8114  caucvgsrlemoffres  8168  caucvgsr  8170  suplocsrlempr  8175  addcnsr  8202  mulcnsr  8203  mulresr  8206  addvalex  8212  pitonnlem1  8213  axi2m1  8243  axcnre  8249  mulcomli  8334  mnfnre  8369  addcomli  8473  add42i  8494  mvrraddi  8545  neg0  8574  negdii  8612  negsubdi2i  8614  crap0  9291  2t2e4  9462  3t2e6  9464  3t3e9  9466  4t2e8  9467  neg1mulneg1e1  9522  8th4div3  9529  halfpm6th  9530  iap0  9533  dfdec10  9785  deceq12i  9790  numltc  9812  decsuc  9817  decsucc  9827  nummac  9831  numma2c  9832  numadd  9833  numaddc  9834  nummul1c  9835  nummul2c  9836  decma  9837  decmac  9838  decma2c  9839  decadd  9840  decaddc  9841  decrmanc  9843  decrmac  9844  decaddci  9847  decsubi  9849  decmul1  9850  decmul1c  9851  decmul2c  9852  11multnc  9854  4t3lem  9883  6t2e12  9890  7t2e14  9895  8t2e16  9901  9t2e18  9908  9t11e99  9916  halfthird  9929  5recm6rec  9930  divfnzn  10031  xnegpnf  10241  xneg0  10244  xaddmnf1  10261  xaddmnf2  10262  mnfaddpnf  10264  iooval2  10328  dfioo2  10387  fzval2  10425  fzsuc2  10497  fztpval  10501  fz0to3un2pr  10541  fz0to4untppr  10542  fzo01  10645  fzo12sn  10646  fzo0to42pr  10649  fldiv4p1lem1div2  10754  intqfrac2  10770  intfracq  10771  xnn0nnen  10888  1tonninf  10892  neg1sqe1  11085  sq2  11086  sq3  11087  cu2  11089  i2  11091  i3  11092  binom2i  11099  sq10  11165  3dec  11167  facp1  11183  fac2  11184  fac4  11186  4bc2eq6  11228  hashp1i  11266  pr0hash2ex  11271  hashfzo  11278  hashxp  11282  hashfibclem  11297  zfz1isolem1  11307  elovmpowrd  11361  ccat1st1st  11424  cji  11683  cnrecnv  11691  sqrt0  11785  resqrexlemover  11791  resqrexlemcalc3  11797  absi  11840  absimle  11866  sumeq12i  12149  summodclem2a  12166  summodc  12168  sum0  12173  fsumsplitf  12193  fsum2dlemstep  12219  fsumabs  12250  fsumiun  12262  0.999...  12306  mertenslem2  12321  prodeq12i  12348  prodmodc  12363  fprod2dlemstep  12407  ege2le3  12456  eft0val  12478  cos0  12515  cos1bnd  12544  cos2bnd  12545  3dvdsdec  12650  3dvds2dec  12651  odd2np1  12658  opoe  12680  nn0o  12692  5ndvds3  12719  5ndvds6  12720  bitsfzolem  12739  m1bits  12745  gcd0val  12755  6gcd4e2  12790  nnmindc  12829  nnminle  12830  3lcm2e6woprm  12882  3lcm2e6  12957  nn0gcdsq  12998  phiprmpw  13022  phimullem  13025  pcprecl  13090  pcprendvds  13091  pcmptdvds  13146  pockthi  13159  4sqlem13m  13204  4sqlem14  13205  4sqlem17  13208  4sqlem18  13209  4sqlem19  13210  dec5nprm  13215  dec2nprm  13216  modxai  13217  modsubi  13221  numexp2x  13227  decsplit0b  13228  decsplit0  13229  decsplit  13231  karatsuba  13232  2exp5  13234  2exp7  13236  2exp8  13237  2exp11  13238  2exp16  13239  3exp3  13240  prmlem0  13242  prmlem1  13244  5prm  13245  11prm  13251  prmlem2  13256  37prm  13257  43prm  13258  83prm  13259  139prm  13260  163prm  13261  317prm  13262  631prm  13263  1259lem1  13264  1259lem2  13265  1259lem3  13266  1259lem4  13267  1259lem5  13268  1259prm  13269  ballotfilemelo  13273  ballotfilem2  13279  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemfval0  13286  ballotfileme  13287  ballotfilemi  13294  ballotfilemsval  13303  ballotfilemrval  13312  ballotfilemrinv  13328  ballotfilemth  13332  ballotfi  13333  unennn  13339  ennnfonelemj0  13343  ennnfonelem0  13347  ennnfonelem1  13349  ennnfonelemhf1o  13355  ennnfonelemrn  13361  ennnfonelemdm  13362  strnfvnd  13423  slotslfn  13429  setsfun  13438  setsfun0  13439  setscom  13443  setsslid  13454  2strstr1g  13527  eqglact  14079  ecqusaddd  14092  ghmeqker  14125  dfrhm2  14512  rmodislmod  14739  cnfldadd  14950  cnfldmul  14952  gsumfsum  14974  expghmap  14993  asclfval  15072  fczpsrbag  15107  cnco  15374  txuni2  15409  txbas  15411  uptx  15427  txcn  15428  cnmptid  15434  cnmpt2t  15446  xmetxp  15660  cnmetdval  15682  remetdval  15700  resubmet  15709  rerestcntop  15711  rerest  15713  divcnap  15718  cnrehmeocntop  15763  dvexp  15864  plyun0  15889  plyco  15912  plycj  15914  sinhalfpilem  15945  cosneghalfpi  15952  efhalfpi  15953  cospi  15954  efipi  15955  eulerid  15956  sin2pi  15957  cos2pi  15958  ef2pi  15959  sincosq4sgn  15983  cosq14gt0  15986  tangtx  15992  sincos4thpi  15994  sincos6thpi  15996  sinkpi  16001  cosq34lt1  16004  dfrelog  16014  2logb9irr  16129  2logb9irrALT  16132  2logb9irrap  16135  log2tlbndlog2  16142  log2ublem2  16144  log2ublem3  16145  log2ublog2  16146  birthdaylem2  16148  birthdaylog2  16150  ppi1  16192  cht1  16193  ppiqub  16215  chtqub  16218  mersenne  16219  perfectlem2  16222  bcp1ctr  16228  bclbnd  16229  zabsle1  16240  lgslem2  16242  lgsfcl2  16247  lgsdir2lem1  16269  lgsdir2lem2  16270  lgsdir2lem4  16272  lgsdir2lem5  16273  lgseisen  16315  2lgslem3a  16334  2lgslem3b  16335  2lgslem3c  16336  2lgslem3d  16337  2lgs2  16343  2lgsoddprmlem3a  16348  2lgsoddprmlem3b  16349  2lgsoddprmlem3c  16350  2lgsoddprmlem3d  16351  pw0ss  16446  umgrislfupgrenlem  16493  vtxdgfval  16651  clwwlknon2  16797  clwwlknon2x  16798  eupth2lembfi  16840  konigsbergvtx  16845  konigsbergiedg  16846  konigsberglem1  16851  konigsberglem2  16852  konigsberglem3  16853  ex-fl  16861  ex-exp  16863  ex-fac  16864  ex-bc  16865  ex-dvds  16866  ex-gcd  16867  bj-dfom  17081  012of  17145  2o01f  17146  pwle2  17150  nninfsellemqall  17180  isomninnlem  17201  iswomninnlem  17221  ismkvnnlem  17224  dceqnconst  17232  dcapnconst  17233  taupi  17245