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 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced 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  3713  dfpr2  3727  disjpr2  3772  rabsnifsb  3776  difprsn1  3852  diftpsn3  3854  difpr  3855  dfuni2  3935  intab  3997  intunsn  4006  rint0  4007  iunid  4066  viin  4070  iinrabm  4073  2iunin  4077  riin0  4082  iunxprg  4091  unopab  4208  cbvmptf  4223  cbvmpt  4224  exmid1stab  4343  unisucg  4557  op1stb  4622  orddif  4692  elxpi  4788  csbxpg  4854  relopabi  4903  inxp  4912  coeq12i  4941  dfdm3  4965  dfrn3  4967  dmun  4986  dmopab  4990  dmopab3  4992  dmxpid  5001  dmxpin  5002  rnopab  5027  rnmpt  5028  rncoss  5051  rncoeq  5054  reseq12i  5059  resundi  5074  resindi  5076  resiun1  5080  resdmdfsn  5104  resopab  5105  opabresid  5114  dfima3  5127  mptima  5136  imadisj  5147  ndmima  5162  mptcnv  5188  rnun  5194  rnuni  5197  imaundi  5198  inimass  5202  cnvxp  5204  rnxpm  5215  dminxp  5230  imainrect  5231  cnvcnv3  5235  dmpropg  5258  op1sta  5267  op2ndb  5269  op2nda  5270  resdmres  5277  mptpreima  5279  coundi  5287  coundir  5288  cocnvcnv1  5296  cores2  5298  dfdm2  5320  iotajust  5334  dfiota2  5336  funi  5407  funtp  5432  fntpg  5435  funcnvuni  5448  funcnvres  5452  imadiflem  5458  imadif  5459  imainlem  5460  imain  5461  fnresdisj  5491  mptfng  5507  fresaunres2disj  5568  resdif  5659  fv2  5688  dffv4g  5690  fveq12i  5699  nfvres  5729  0fv  5731  dfimafn2  5749  fnimapr  5760  fvmptss2  5777  fvmptg  5778  fvmpts  5780  fvmpt2  5786  mptfvex  5788  elfvmptrab  5798  fvopab6  5799  f1ompt  5853  dfmpt  5880  ressnop0  5890  fprg  5892  fvsnun1  5906  fsnunfv  5910  fvpr2g  5916  imauni  5961  fliftfuns  5998  cbvriota  6044  oveq123i  6093  fconstmpo  6177  resoprab  6178  mpofun  6184  rnmpo  6193  reldmmpo  6194  ov  6202  ovigg  6203  ovmpt4g  6205  ovg  6222  caov31  6273  elmpocl  6278  f1ocnvd  6286  oprabrexex2  6357  op1st  6374  op2nd  6375  f1stres  6387  f2ndres  6388  unielxp  6402  dfoprab3s  6418  dfoprab4  6420  mpompts  6428  mpofvex  6435  oprab2co  6448  df1st2  6449  df2nd2  6450  f1od2  6465  elmpom  6468  cnvimadfsn  6479  brtpos0  6517  tposoprab  6545  smores3  6558  tfrlemi14d  6598  tfr1onlemaccex  6613  tfrcllemaccex  6626  rdgisuc1  6649  rdg0  6652  frec0g  6662  df1o2  6695  df2o2  6697  oasuc  6731  omv2  6732  omsuc  6739  ecidsn  6850  qliftfuns  6887  oviec  6909  mapsncnv  6971  dfixp  6976  xpcomco  7118  xpassen  7122  ssenen  7146  undifdc  7225  unfiin  7227  fidcenumlemrks  7264  fidcenumlemr  7266  sbthlemi5  7272  sbthlemi8  7275  fi0  7303  inf00  7365  djuf1olemr  7388  djuinr  7397  djuin  7398  djuun  7401  casefun  7419  casedm  7420  caseinj  7423  caseinl  7425  caseinr  7426  endjusym  7430  eninl  7431  eninr  7432  djudm  7439  djuinj  7440  fodjuomni  7483  fodjumkv  7494  nninfwlporlemd  7506  pm54.43  7530  exmidfodomrlemim  7547  xp2dju  7565  djucomen  7566  djuassen  7567  xpdjuen  7568  pw1nel3  7584  sucpw1nel3  7586  addpiord  7677  mulpiord  7678  dmaddpi  7686  dmmulpi  7687  recmulnqg  7752  1lt2nq  7767  halfnqq  7771  dfmq0qs  7790  dfplq0qs  7791  genpdf  7869  1prl  7916  1pru  7917  ltexprlemell  7959  ltexprlemelu  7960  recexprlemell  7983  recexprlemelu  7984  cauappcvgprlemm  8006  cauappcvgprlemopl  8007  cauappcvgprlemlol  8008  cauappcvgprlemopu  8009  cauappcvgprlemupu  8010  cauappcvgprlemdisj  8012  cauappcvgprlemloc  8013  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  cauappcvgprlemladdrl  8018  cauappcvgprlem2  8021  caucvgprlemm  8029  caucvgprlemopl  8030  caucvgprlemlol  8031  caucvgprlemopu  8032  caucvgprlemupu  8033  caucvgprlemdisj  8035  caucvgprlemloc  8036  caucvgprlemcl  8037  caucvgprlemladdfu  8038  caucvgprlemladdrl  8039  caucvgprlem2  8041  caucvgprprlemell  8046  caucvgprprlemelu  8047  caucvgprprlemml  8055  caucvgprprlemmu  8056  caucvgprprlemclphr  8066  caucvgprprlemexbt  8067  caucvgprprlem2  8071  addsrpr  8106  mulsrpr  8107  caucvgsrlemoffres  8161  caucvgsr  8163  suplocsrlempr  8168  addcnsr  8195  mulcnsr  8196  mulresr  8199  addvalex  8205  pitonnlem1  8206  axi2m1  8236  axcnre  8242  mulcomli  8327  mnfnre  8362  addcomli  8465  add42i  8486  mvrraddi  8537  neg0  8566  negdii  8604  negsubdi2i  8606  crap0  9282  2t2e4  9442  3t2e6  9444  3t3e9  9445  4t2e8  9446  neg1mulneg1e1  9500  8th4div3  9507  halfpm6th  9508  iap0  9511  dfdec10  9763  deceq12i  9768  numltc  9785  decsuc  9790  decsucc  9800  nummac  9804  numma2c  9805  numadd  9806  numaddc  9807  nummul1c  9808  nummul2c  9809  decma  9810  decmac  9811  decma2c  9812  decadd  9813  decaddc  9814  decrmanc  9816  decrmac  9817  decaddci  9820  decsubi  9822  decmul1  9823  decmul1c  9824  decmul2c  9825  11multnc  9827  4t3lem  9856  6t2e12  9863  7t2e14  9868  8t2e16  9874  9t2e18  9881  9t11e99  9889  halfthird  9902  5recm6rec  9903  divfnzn  10004  xnegpnf  10213  xneg0  10216  xaddmnf1  10233  xaddmnf2  10234  mnfaddpnf  10236  iooval2  10300  dfioo2  10359  fzval2  10397  fzsuc2  10469  fztpval  10473  fz0to3un2pr  10513  fz0to4untppr  10514  fzo01  10617  fzo12sn  10618  fzo0to42pr  10621  fldiv4p1lem1div2  10723  intqfrac2  10739  intfracq  10740  xnn0nnen  10857  1tonninf  10861  neg1sqe1  11054  sq2  11055  sq3  11056  cu2  11058  i2  11060  i3  11061  binom2i  11068  sq10  11133  3dec  11135  facp1  11151  fac2  11152  fac4  11154  4bc2eq6  11196  hashp1i  11234  pr0hash2ex  11239  hashfzo  11246  hashxp  11250  hashfibclem  11265  zfz1isolem1  11275  elovmpowrd  11329  ccat1st1st  11392  cji  11651  cnrecnv  11659  sqrt0  11753  resqrexlemover  11759  resqrexlemcalc3  11765  absi  11808  absimle  11833  sumeq12i  12114  summodclem2a  12131  summodc  12133  sum0  12138  fsumsplitf  12158  fsum2dlemstep  12184  fsumabs  12215  fsumiun  12227  0.999...  12271  mertenslem2  12286  prodeq12i  12313  prodmodc  12328  fprod2dlemstep  12372  ege2le3  12421  eft0val  12443  cos0  12480  cos1bnd  12509  cos2bnd  12510  3dvdsdec  12615  3dvds2dec  12616  odd2np1  12623  opoe  12645  nn0o  12657  5ndvds3  12684  5ndvds6  12685  bitsfzolem  12704  m1bits  12710  gcd0val  12720  6gcd4e2  12755  nnmindc  12794  nnminle  12795  3lcm2e6woprm  12847  3lcm2e6  12921  nn0gcdsq  12961  phiprmpw  12983  phimullem  12986  pcprecl  13051  pcprendvds  13052  pcmptdvds  13107  pockthi  13120  4sqlem13m  13165  4sqlem14  13166  4sqlem17  13169  4sqlem18  13170  4sqlem19  13171  dec5nprm  13176  dec2nprm  13177  modxai  13178  modsubi  13181  numexp2x  13187  decsplit0b  13188  decsplit0  13189  decsplit  13191  karatsuba  13192  2exp5  13194  2exp7  13196  2exp8  13197  2exp11  13198  2exp16  13199  3exp3  13200  ballotfilemelo  13205  ballotfilem2  13211  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemfval0  13218  ballotfileme  13219  ballotfilemi  13226  ballotfilemsval  13235  ballotfilemrval  13244  ballotfilemrinv  13260  ballotfilemth  13264  ballotfi  13265  unennn  13271  ennnfonelemj0  13275  ennnfonelem0  13279  ennnfonelem1  13281  ennnfonelemhf1o  13287  ennnfonelemrn  13293  ennnfonelemdm  13294  strnfvnd  13355  slotslfn  13361  setsfun  13370  setsfun0  13371  setscom  13375  setsslid  13386  2strstr1g  13459  eqglact  14011  ecqusaddd  14024  ghmeqker  14057  dfrhm2  14444  rmodislmod  14671  cnfldadd  14882  cnfldmul  14884  gsumfsum  14906  expghmap  14925  asclfval  15004  fczpsrbag  15039  cnco  15305  txuni2  15340  txbas  15342  uptx  15358  txcn  15359  cnmptid  15365  cnmpt2t  15377  xmetxp  15591  cnmetdval  15613  remetdval  15631  resubmet  15640  rerestcntop  15642  rerest  15644  divcnap  15649  cnrehmeocntop  15694  dvexp  15795  plyun0  15820  plyco  15843  plycj  15845  sinhalfpilem  15875  cosneghalfpi  15882  efhalfpi  15883  cospi  15884  efipi  15885  eulerid  15886  sin2pi  15887  cos2pi  15888  ef2pi  15889  sincosq4sgn  15913  cosq14gt0  15916  tangtx  15922  sincos4thpi  15924  sincos6thpi  15926  sinkpi  15931  cosq34lt1  15934  dfrelog  15944  2logb9irr  16056  2logb9irrALT  16059  2logb9irrap  16062  log2tlbndlog2  16065  log2ublem2  16067  log2ublem3  16068  log2ublog2  16069  birthdaylem2  16071  birthdaylog2  16073  mersenne  16094  perfectlem2  16097  zabsle1  16101  lgslem2  16103  lgsfcl2  16108  lgsdir2lem1  16130  lgsdir2lem2  16131  lgsdir2lem4  16133  lgsdir2lem5  16134  lgseisen  16176  2lgslem3a  16195  2lgslem3b  16196  2lgslem3c  16197  2lgslem3d  16198  2lgs2  16204  2lgsoddprmlem3a  16209  2lgsoddprmlem3b  16210  2lgsoddprmlem3c  16211  2lgsoddprmlem3d  16212  pw0ss  16307  umgrislfupgrenlem  16354  vtxdgfval  16512  clwwlknon2  16658  clwwlknon2x  16659  eupth2lembfi  16701  konigsbergvtx  16706  konigsbergiedg  16707  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  ex-fl  16722  ex-exp  16724  ex-fac  16725  ex-bc  16726  ex-dvds  16727  ex-gcd  16728  bj-dfom  16942  012of  17006  2o01f  17007  pwle2  17011  nninfsellemqall  17032  isomninnlem  17053  iswomninnlem  17073  ismkvnnlem  17076  dceqnconst  17084  dcapnconst  17085  taupi  17097