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  3806  diftpsn3  3808  difpr  3809  dfuni2  3889  intab  3951  intunsn  3960  rint0  3961  iunid  4020  viin  4024  iinrabm  4027  2iunin  4031  riin0  4036  iunxprg  4045  unopab  4162  cbvmptf  4177  cbvmpt  4178  exmid1stab  4291  unisucg  4502  op1stb  4566  orddif  4636  elxpi  4732  csbxpg  4797  relopabi  4844  inxp  4853  coeq12i  4882  dfdm3  4906  dfrn3  4908  dmun  4927  dmopab  4931  dmopab3  4933  dmxpid  4941  dmxpin  4942  rnopab  4967  rnmpt  4968  rncoss  4991  rncoeq  4994  reseq12i  4999  resundi  5014  resindi  5016  resiun1  5020  resdmdfsn  5044  resopab  5045  opabresid  5054  dfima3  5067  mptima  5076  imadisj  5086  ndmima  5101  mptcnv  5127  rnun  5133  rnuni  5136  imaundi  5137  inimass  5141  cnvxp  5143  rnxpm  5154  dminxp  5169  imainrect  5170  cnvcnv3  5174  dmpropg  5197  op1sta  5206  op2ndb  5208  op2nda  5209  resdmres  5216  mptpreima  5218  coundi  5226  coundir  5227  cocnvcnv1  5235  cores2  5237  dfdm2  5259  iotajust  5273  dfiota2  5275  funi  5346  funtp  5370  fntpg  5373  funcnvuni  5386  funcnvres  5390  imadiflem  5396  imadif  5397  imainlem  5398  imain  5399  fnresdisj  5429  mptfng  5445  resdif  5590  fv2  5618  dffv4g  5620  fveq12i  5629  nfvres  5657  0fv  5659  dfimafn2  5676  fnimapr  5687  fvmptss2  5702  fvmptg  5703  fvmpts  5705  fvmpt2  5711  mptfvex  5713  elfvmptrab  5723  fvopab6  5724  f1ompt  5779  dfmpt  5805  ressnop0  5813  fprg  5815  fvsnun1  5829  fsnunfv  5833  fvpr2g  5839  imauni  5878  fliftfuns  5915  cbvriota  5959  oveq123i  6008  fconstmpo  6090  resoprab  6091  mpofun  6097  rnmpo  6106  reldmmpo  6107  ov  6115  ovigg  6116  ovmpt4g  6118  ovg  6135  caov31  6186  elmpocl  6191  f1ocnvd  6198  oprabrexex2  6265  op1st  6282  op2nd  6283  f1stres  6295  f2ndres  6296  unielxp  6310  dfoprab3s  6326  dfoprab4  6328  mpompts  6334  mpofvex  6341  oprab2co  6354  df1st2  6355  df2nd2  6356  f1od2  6371  brtpos0  6388  tposoprab  6416  smores3  6429  tfrlemi14d  6469  tfr1onlemaccex  6484  tfrcllemaccex  6497  rdgisuc1  6520  rdg0  6523  frec0g  6533  df1o2  6565  df2o2  6567  oasuc  6600  omv2  6601  omsuc  6608  ecidsn  6719  qliftfuns  6756  oviec  6778  mapsncnv  6832  dfixp  6837  xpcomco  6973  xpassen  6977  ssenen  7000  undifdc  7074  unfiin  7076  fidcenumlemrks  7108  fidcenumlemr  7110  sbthlemi5  7116  sbthlemi8  7119  fi0  7130  inf00  7186  djuf1olemr  7209  djuinr  7218  djuin  7219  djuun  7222  casefun  7240  casedm  7241  caseinj  7244  caseinl  7246  caseinr  7247  endjusym  7251  eninl  7252  eninr  7253  djudm  7260  djuinj  7261  fodjuomni  7304  fodjumkv  7315  nninfwlporlemd  7327  pm54.43  7351  exmidfodomrlemim  7367  xp2dju  7385  djucomen  7386  djuassen  7387  xpdjuen  7388  pw1nel3  7404  sucpw1nel3  7406  addpiord  7491  mulpiord  7492  dmaddpi  7500  dmmulpi  7501  recmulnqg  7566  1lt2nq  7581  halfnqq  7585  dfmq0qs  7604  dfplq0qs  7605  genpdf  7683  1prl  7730  1pru  7731  ltexprlemell  7773  ltexprlemelu  7774  recexprlemell  7797  recexprlemelu  7798  cauappcvgprlemm  7820  cauappcvgprlemopl  7821  cauappcvgprlemlol  7822  cauappcvgprlemopu  7823  cauappcvgprlemupu  7824  cauappcvgprlemdisj  7826  cauappcvgprlemloc  7827  cauappcvgprlemladdfu  7829  cauappcvgprlemladdfl  7830  cauappcvgprlemladdrl  7832  cauappcvgprlem2  7835  caucvgprlemm  7843  caucvgprlemopl  7844  caucvgprlemlol  7845  caucvgprlemopu  7846  caucvgprlemupu  7847  caucvgprlemdisj  7849  caucvgprlemloc  7850  caucvgprlemcl  7851  caucvgprlemladdfu  7852  caucvgprlemladdrl  7853  caucvgprlem2  7855  caucvgprprlemell  7860  caucvgprprlemelu  7861  caucvgprprlemml  7869  caucvgprprlemmu  7870  caucvgprprlemclphr  7880  caucvgprprlemexbt  7881  caucvgprprlem2  7885  addsrpr  7920  mulsrpr  7921  caucvgsrlemoffres  7975  caucvgsr  7977  suplocsrlempr  7982  addcnsr  8009  mulcnsr  8010  mulresr  8013  addvalex  8019  pitonnlem1  8020  axi2m1  8050  axcnre  8056  mulcomli  8141  mnfnre  8177  addcomli  8279  add42i  8300  mvrraddi  8351  neg0  8380  negdii  8418  negsubdi2i  8420  crap0  9093  2t2e4  9253  3t2e6  9255  3t3e9  9256  4t2e8  9257  neg1mulneg1e1  9311  8th4div3  9318  halfpm6th  9319  iap0  9322  dfdec10  9569  deceq12i  9574  numltc  9591  decsuc  9596  decsucc  9606  nummac  9610  numma2c  9611  numadd  9612  numaddc  9613  nummul1c  9614  nummul2c  9615  decma  9616  decmac  9617  decma2c  9618  decadd  9619  decaddc  9620  decrmanc  9622  decrmac  9623  decaddci  9626  decsubi  9628  decmul1  9629  decmul1c  9630  decmul2c  9631  11multnc  9633  4t3lem  9662  6t2e12  9669  7t2e14  9674  8t2e16  9680  9t2e18  9687  9t11e99  9695  halfthird  9708  5recm6rec  9709  divfnzn  9804  xnegpnf  10012  xneg0  10015  xaddmnf1  10032  xaddmnf2  10033  mnfaddpnf  10035  iooval2  10099  dfioo2  10158  fzval2  10195  fzsuc2  10263  fztpval  10267  fz0to3un2pr  10307  fz0to4untppr  10308  fzo01  10409  fzo12sn  10410  fzo0to42pr  10413  fldiv4p1lem1div2  10512  intqfrac2  10528  intfracq  10529  xnn0nnen  10646  1tonninf  10650  neg1sqe1  10843  sq2  10844  sq3  10845  cu2  10847  i2  10849  i3  10850  binom2i  10857  sq10  10921  3dec  10923  facp1  10939  fac2  10940  fac4  10942  4bc2eq6  10983  hashp1i  11019  pr0hash2ex  11024  hashfzo  11031  hashxp  11035  zfz1isolem1  11049  elovmpowrd  11099  ccat1st1st  11158  cji  11399  cnrecnv  11407  sqrt0  11501  resqrexlemover  11507  resqrexlemcalc3  11513  absi  11556  absimle  11581  sumeq12i  11862  summodclem2a  11878  summodc  11880  sum0  11885  fsumsplitf  11905  fsum2dlemstep  11931  fsumabs  11962  fsumiun  11974  0.999...  12018  mertenslem2  12033  prodeq12i  12060  prodmodc  12075  fprod2dlemstep  12119  ege2le3  12168  eft0val  12190  cos0  12227  cos1bnd  12256  cos2bnd  12257  3dvdsdec  12362  3dvds2dec  12363  odd2np1  12370  opoe  12392  nn0o  12404  5ndvds3  12431  5ndvds6  12432  bitsfzolem  12451  m1bits  12457  gcd0val  12467  6gcd4e2  12502  nnmindc  12541  nnminle  12542  3lcm2e6woprm  12594  3lcm2e6  12668  nn0gcdsq  12708  phiprmpw  12730  phimullem  12733  pcprecl  12798  pcprendvds  12799  pcmptdvds  12854  pockthi  12867  4sqlem13m  12912  4sqlem14  12913  4sqlem17  12916  4sqlem18  12917  4sqlem19  12918  dec5nprm  12923  dec2nprm  12924  modxai  12925  modsubi  12928  numexp2x  12934  decsplit0b  12935  decsplit0  12936  decsplit  12938  karatsuba  12939  2exp5  12941  2exp7  12943  2exp8  12944  2exp11  12945  2exp16  12946  3exp3  12947  unennn  12954  ennnfonelemj0  12958  ennnfonelem0  12962  ennnfonelem1  12964  ennnfonelemhf1o  12970  ennnfonelemrn  12976  ennnfonelemdm  12977  strnfvnd  13038  slotslfn  13044  setsfun  13053  setsfun0  13054  setscom  13058  setsslid  13069  2strstr1g  13141  eqglact  13748  ecqusaddd  13761  ghmeqker  13794  dfrhm2  14103  rmodislmod  14300  cnfldadd  14511  cnfldmul  14513  expghmap  14556  fczpsrbag  14620  cnco  14880  txuni2  14915  txbas  14917  uptx  14933  txcn  14934  cnmptid  14940  cnmpt2t  14952  xmetxp  15166  cnmetdval  15188  remetdval  15206  resubmet  15215  rerestcntop  15217  rerest  15219  divcnap  15224  cnrehmeocntop  15269  dvexp  15370  plyun0  15395  plyco  15418  plycj  15420  sinhalfpilem  15450  cosneghalfpi  15457  efhalfpi  15458  cospi  15459  efipi  15460  eulerid  15461  sin2pi  15462  cos2pi  15463  ef2pi  15464  sincosq4sgn  15488  cosq14gt0  15491  tangtx  15497  sincos4thpi  15499  sincos6thpi  15501  sinkpi  15506  cosq34lt1  15509  dfrelog  15519  2logb9irr  15630  2logb9irrALT  15633  2logb9irrap  15636  mersenne  15656  perfectlem2  15659  zabsle1  15663  lgslem2  15665  lgsfcl2  15670  lgsdir2lem1  15692  lgsdir2lem2  15693  lgsdir2lem4  15695  lgsdir2lem5  15696  lgseisen  15738  2lgslem3a  15757  2lgslem3b  15758  2lgslem3c  15759  2lgslem3d  15760  2lgs2  15766  2lgsoddprmlem3a  15771  2lgsoddprmlem3b  15772  2lgsoddprmlem3c  15773  2lgsoddprmlem3d  15774  pw0ss  15868  umgrislfupgrenlem  15913  ex-fl  16019  ex-exp  16021  ex-fac  16022  ex-bc  16023  ex-dvds  16024  ex-gcd  16025  bj-dfom  16226  012of  16288  2o01f  16289  pwle2  16295  nninfsellemqall  16312  isomninnlem  16329  iswomninnlem  16348  ismkvnnlem  16351  dceqnconst  16359  dcapnconst  16360  taupi  16372