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  4292  unisucg  4505  op1stb  4569  orddif  4639  elxpi  4735  csbxpg  4800  relopabi  4847  inxp  4856  coeq12i  4885  dfdm3  4909  dfrn3  4911  dmun  4930  dmopab  4934  dmopab3  4936  dmxpid  4945  dmxpin  4946  rnopab  4971  rnmpt  4972  rncoss  4995  rncoeq  4998  reseq12i  5003  resundi  5018  resindi  5020  resiun1  5024  resdmdfsn  5048  resopab  5049  opabresid  5058  dfima3  5071  mptima  5080  imadisj  5090  ndmima  5105  mptcnv  5131  rnun  5137  rnuni  5140  imaundi  5141  inimass  5145  cnvxp  5147  rnxpm  5158  dminxp  5173  imainrect  5174  cnvcnv3  5178  dmpropg  5201  op1sta  5210  op2ndb  5212  op2nda  5213  resdmres  5220  mptpreima  5222  coundi  5230  coundir  5231  cocnvcnv1  5239  cores2  5241  dfdm2  5263  iotajust  5277  dfiota2  5279  funi  5350  funtp  5374  fntpg  5377  funcnvuni  5390  funcnvres  5394  imadiflem  5400  imadif  5401  imainlem  5402  imain  5403  fnresdisj  5433  mptfng  5449  resdif  5596  fv2  5624  dffv4g  5626  fveq12i  5635  nfvres  5665  0fv  5667  dfimafn2  5685  fnimapr  5696  fvmptss2  5711  fvmptg  5712  fvmpts  5714  fvmpt2  5720  mptfvex  5722  elfvmptrab  5732  fvopab6  5733  f1ompt  5788  dfmpt  5814  ressnop0  5824  fprg  5826  fvsnun1  5840  fsnunfv  5844  fvpr2g  5850  imauni  5891  fliftfuns  5928  cbvriota  5972  oveq123i  6021  fconstmpo  6105  resoprab  6106  mpofun  6112  rnmpo  6121  reldmmpo  6122  ov  6130  ovigg  6131  ovmpt4g  6133  ovg  6150  caov31  6201  elmpocl  6206  f1ocnvd  6214  oprabrexex2  6281  op1st  6298  op2nd  6299  f1stres  6311  f2ndres  6312  unielxp  6326  dfoprab3s  6342  dfoprab4  6344  mpompts  6350  mpofvex  6357  oprab2co  6370  df1st2  6371  df2nd2  6372  f1od2  6387  brtpos0  6404  tposoprab  6432  smores3  6445  tfrlemi14d  6485  tfr1onlemaccex  6500  tfrcllemaccex  6513  rdgisuc1  6536  rdg0  6539  frec0g  6549  df1o2  6582  df2o2  6584  oasuc  6618  omv2  6619  omsuc  6626  ecidsn  6737  qliftfuns  6774  oviec  6796  mapsncnv  6850  dfixp  6855  xpcomco  6993  xpassen  6997  ssenen  7020  undifdc  7094  unfiin  7096  fidcenumlemrks  7128  fidcenumlemr  7130  sbthlemi5  7136  sbthlemi8  7139  fi0  7150  inf00  7206  djuf1olemr  7229  djuinr  7238  djuin  7239  djuun  7242  casefun  7260  casedm  7261  caseinj  7264  caseinl  7266  caseinr  7267  endjusym  7271  eninl  7272  eninr  7273  djudm  7280  djuinj  7281  fodjuomni  7324  fodjumkv  7335  nninfwlporlemd  7347  pm54.43  7371  exmidfodomrlemim  7387  xp2dju  7405  djucomen  7406  djuassen  7407  xpdjuen  7408  pw1nel3  7424  sucpw1nel3  7426  addpiord  7511  mulpiord  7512  dmaddpi  7520  dmmulpi  7521  recmulnqg  7586  1lt2nq  7601  halfnqq  7605  dfmq0qs  7624  dfplq0qs  7625  genpdf  7703  1prl  7750  1pru  7751  ltexprlemell  7793  ltexprlemelu  7794  recexprlemell  7817  recexprlemelu  7818  cauappcvgprlemm  7840  cauappcvgprlemopl  7841  cauappcvgprlemlol  7842  cauappcvgprlemopu  7843  cauappcvgprlemupu  7844  cauappcvgprlemdisj  7846  cauappcvgprlemloc  7847  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  cauappcvgprlemladdrl  7852  cauappcvgprlem2  7855  caucvgprlemm  7863  caucvgprlemopl  7864  caucvgprlemlol  7865  caucvgprlemopu  7866  caucvgprlemupu  7867  caucvgprlemdisj  7869  caucvgprlemloc  7870  caucvgprlemcl  7871  caucvgprlemladdfu  7872  caucvgprlemladdrl  7873  caucvgprlem2  7875  caucvgprprlemell  7880  caucvgprprlemelu  7881  caucvgprprlemml  7889  caucvgprprlemmu  7890  caucvgprprlemclphr  7900  caucvgprprlemexbt  7901  caucvgprprlem2  7905  addsrpr  7940  mulsrpr  7941  caucvgsrlemoffres  7995  caucvgsr  7997  suplocsrlempr  8002  addcnsr  8029  mulcnsr  8030  mulresr  8033  addvalex  8039  pitonnlem1  8040  axi2m1  8070  axcnre  8076  mulcomli  8161  mnfnre  8197  addcomli  8299  add42i  8320  mvrraddi  8371  neg0  8400  negdii  8438  negsubdi2i  8440  crap0  9113  2t2e4  9273  3t2e6  9275  3t3e9  9276  4t2e8  9277  neg1mulneg1e1  9331  8th4div3  9338  halfpm6th  9339  iap0  9342  dfdec10  9589  deceq12i  9594  numltc  9611  decsuc  9616  decsucc  9626  nummac  9630  numma2c  9631  numadd  9632  numaddc  9633  nummul1c  9634  nummul2c  9635  decma  9636  decmac  9637  decma2c  9638  decadd  9639  decaddc  9640  decrmanc  9642  decrmac  9643  decaddci  9646  decsubi  9648  decmul1  9649  decmul1c  9650  decmul2c  9651  11multnc  9653  4t3lem  9682  6t2e12  9689  7t2e14  9694  8t2e16  9700  9t2e18  9707  9t11e99  9715  halfthird  9728  5recm6rec  9729  divfnzn  9824  xnegpnf  10032  xneg0  10035  xaddmnf1  10052  xaddmnf2  10053  mnfaddpnf  10055  iooval2  10119  dfioo2  10178  fzval2  10215  fzsuc2  10283  fztpval  10287  fz0to3un2pr  10327  fz0to4untppr  10328  fzo01  10430  fzo12sn  10431  fzo0to42pr  10434  fldiv4p1lem1div2  10533  intqfrac2  10549  intfracq  10550  xnn0nnen  10667  1tonninf  10671  neg1sqe1  10864  sq2  10865  sq3  10866  cu2  10868  i2  10870  i3  10871  binom2i  10878  sq10  10942  3dec  10944  facp1  10960  fac2  10961  fac4  10963  4bc2eq6  11004  hashp1i  11040  pr0hash2ex  11045  hashfzo  11052  hashxp  11056  zfz1isolem1  11070  elovmpowrd  11121  ccat1st1st  11180  cji  11421  cnrecnv  11429  sqrt0  11523  resqrexlemover  11529  resqrexlemcalc3  11535  absi  11578  absimle  11603  sumeq12i  11884  summodclem2a  11900  summodc  11902  sum0  11907  fsumsplitf  11927  fsum2dlemstep  11953  fsumabs  11984  fsumiun  11996  0.999...  12040  mertenslem2  12055  prodeq12i  12082  prodmodc  12097  fprod2dlemstep  12141  ege2le3  12190  eft0val  12212  cos0  12249  cos1bnd  12278  cos2bnd  12279  3dvdsdec  12384  3dvds2dec  12385  odd2np1  12392  opoe  12414  nn0o  12426  5ndvds3  12453  5ndvds6  12454  bitsfzolem  12473  m1bits  12479  gcd0val  12489  6gcd4e2  12524  nnmindc  12563  nnminle  12564  3lcm2e6woprm  12616  3lcm2e6  12690  nn0gcdsq  12730  phiprmpw  12752  phimullem  12755  pcprecl  12820  pcprendvds  12821  pcmptdvds  12876  pockthi  12889  4sqlem13m  12934  4sqlem14  12935  4sqlem17  12938  4sqlem18  12939  4sqlem19  12940  dec5nprm  12945  dec2nprm  12946  modxai  12947  modsubi  12950  numexp2x  12956  decsplit0b  12957  decsplit0  12958  decsplit  12960  karatsuba  12961  2exp5  12963  2exp7  12965  2exp8  12966  2exp11  12967  2exp16  12968  3exp3  12969  unennn  12976  ennnfonelemj0  12980  ennnfonelem0  12984  ennnfonelem1  12986  ennnfonelemhf1o  12992  ennnfonelemrn  12998  ennnfonelemdm  12999  strnfvnd  13060  slotslfn  13066  setsfun  13075  setsfun0  13076  setscom  13080  setsslid  13091  2strstr1g  13163  eqglact  13770  ecqusaddd  13783  ghmeqker  13816  dfrhm2  14126  rmodislmod  14323  cnfldadd  14534  cnfldmul  14536  expghmap  14579  fczpsrbag  14643  cnco  14903  txuni2  14938  txbas  14940  uptx  14956  txcn  14957  cnmptid  14963  cnmpt2t  14975  xmetxp  15189  cnmetdval  15211  remetdval  15229  resubmet  15238  rerestcntop  15240  rerest  15242  divcnap  15247  cnrehmeocntop  15292  dvexp  15393  plyun0  15418  plyco  15441  plycj  15443  sinhalfpilem  15473  cosneghalfpi  15480  efhalfpi  15481  cospi  15482  efipi  15483  eulerid  15484  sin2pi  15485  cos2pi  15486  ef2pi  15487  sincosq4sgn  15511  cosq14gt0  15514  tangtx  15520  sincos4thpi  15522  sincos6thpi  15524  sinkpi  15529  cosq34lt1  15532  dfrelog  15542  2logb9irr  15653  2logb9irrALT  15656  2logb9irrap  15659  mersenne  15679  perfectlem2  15682  zabsle1  15686  lgslem2  15688  lgsfcl2  15693  lgsdir2lem1  15715  lgsdir2lem2  15716  lgsdir2lem4  15718  lgsdir2lem5  15719  lgseisen  15761  2lgslem3a  15780  2lgslem3b  15781  2lgslem3c  15782  2lgslem3d  15783  2lgs2  15789  2lgsoddprmlem3a  15794  2lgsoddprmlem3b  15795  2lgsoddprmlem3c  15796  2lgsoddprmlem3d  15797  pw0ss  15891  umgrislfupgrenlem  15936  ex-fl  16113  ex-exp  16115  ex-fac  16116  ex-bc  16117  ex-dvds  16118  ex-gcd  16119  bj-dfom  16320  012of  16386  2o01f  16387  pwle2  16393  nninfsellemqall  16411  isomninnlem  16428  iswomninnlem  16447  ismkvnnlem  16450  dceqnconst  16458  dcapnconst  16459  taupi  16471