Theorem eqtri 2252

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  eqtr2i  2253  eqtr3i  2254  eqtr4i  2255  3eqtri  2256  3eqtrri  2257  3eqtr2i  2258  cbvrab  2801  csb2  3130  cbvrabcsf  3194  difjust  3202  unjust  3204  injust  3206  dfdif3  3319  difeq12i  3325  inrot  3424  symdif1  3474  rabnc  3529  0in  3532  ssdifin0  3578  dfif3  3623  ifbieq2i  3633  ifbieq12i  3635  pwjust  3657  snjust  3678  dfpr2  3692  disjpr2  3737  rabsnifsb  3741  difprsn1  3817  diftpsn3  3819  difpr  3820  dfuni2  3900  intab  3962  intunsn  3971  rint0  3972  iunid  4031  viin  4035  iinrabm  4038  2iunin  4042  riin0  4047  iunxprg  4056  unopab  4173  cbvmptf  4188  cbvmpt  4189  exmid1stab  4304  unisucg  4517  op1stb  4581  orddif  4651  elxpi  4747  csbxpg  4813  relopabi  4861  inxp  4870  coeq12i  4899  dfdm3  4923  dfrn3  4925  dmun  4944  dmopab  4948  dmopab3  4950  dmxpid  4959  dmxpin  4960  rnopab  4985  rnmpt  4986  rncoss  5009  rncoeq  5012  reseq12i  5017  resundi  5032  resindi  5034  resiun1  5038  resdmdfsn  5062  resopab  5063  opabresid  5072  dfima3  5085  mptima  5094  imadisj  5105  ndmima  5120  mptcnv  5146  rnun  5152  rnuni  5155  imaundi  5156  inimass  5160  cnvxp  5162  rnxpm  5173  dminxp  5188  imainrect  5189  cnvcnv3  5193  dmpropg  5216  op1sta  5225  op2ndb  5227  op2nda  5228  resdmres  5235  mptpreima  5237  coundi  5245  coundir  5246  cocnvcnv1  5254  cores2  5256  dfdm2  5278  iotajust  5292  dfiota2  5294  funi  5365  funtp  5390  fntpg  5393  funcnvuni  5406  funcnvres  5410  imadiflem  5416  imadif  5417  imainlem  5418  imain  5419  fnresdisj  5449  mptfng  5465  resdif  5614  fv2  5643  dffv4g  5645  fveq12i  5654  nfvres  5684  0fv  5686  dfimafn2  5704  fnimapr  5715  fvmptss2  5730  fvmptg  5731  fvmpts  5733  fvmpt2  5739  mptfvex  5741  elfvmptrab  5751  fvopab6  5752  f1ompt  5806  dfmpt  5833  ressnop0  5843  fprg  5845  fvsnun1  5859  fsnunfv  5863  fvpr2g  5869  imauni  5912  fliftfuns  5949  cbvriota  5993  oveq123i  6042  fconstmpo  6126  resoprab  6127  mpofun  6133  rnmpo  6142  reldmmpo  6143  ov  6151  ovigg  6152  ovmpt4g  6154  ovg  6171  caov31  6222  elmpocl  6227  f1ocnvd  6235  oprabrexex2  6301  op1st  6318  op2nd  6319  f1stres  6331  f2ndres  6332  unielxp  6346  dfoprab3s  6362  dfoprab4  6364  mpompts  6372  mpofvex  6379  oprab2co  6392  df1st2  6393  df2nd2  6394  f1od2  6409  elmpom  6412  cnvimadfsn  6423  brtpos0  6461  tposoprab  6489  smores3  6502  tfrlemi14d  6542  tfr1onlemaccex  6557  tfrcllemaccex  6570  rdgisuc1  6593  rdg0  6596  frec0g  6606  df1o2  6639  df2o2  6641  oasuc  6675  omv2  6676  omsuc  6683  ecidsn  6794  qliftfuns  6831  oviec  6853  mapsncnv  6907  dfixp  6912  xpcomco  7053  xpassen  7057  ssenen  7080  undifdc  7159  unfiin  7161  fidcenumlemrks  7195  fidcenumlemr  7197  sbthlemi5  7203  sbthlemi8  7206  fi0  7217  inf00  7273  djuf1olemr  7296  djuinr  7305  djuin  7306  djuun  7309  casefun  7327  casedm  7328  caseinj  7331  caseinl  7333  caseinr  7334  endjusym  7338  eninl  7339  eninr  7340  djudm  7347  djuinj  7348  fodjuomni  7391  fodjumkv  7402  nninfwlporlemd  7414  pm54.43  7438  exmidfodomrlemim  7455  xp2dju  7473  djucomen  7474  djuassen  7475  xpdjuen  7476  pw1nel3  7492  sucpw1nel3  7494  addpiord  7579  mulpiord  7580  dmaddpi  7588  dmmulpi  7589  recmulnqg  7654  1lt2nq  7669  halfnqq  7673  dfmq0qs  7692  dfplq0qs  7693  genpdf  7771  1prl  7818  1pru  7819  ltexprlemell  7861  ltexprlemelu  7862  recexprlemell  7885  recexprlemelu  7886  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdrl  7920  cauappcvgprlem2  7923  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem2  7943  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  caucvgprprlem2  7973  addsrpr  8008  mulsrpr  8009  caucvgsrlemoffres  8063  caucvgsr  8065  suplocsrlempr  8070  addcnsr  8097  mulcnsr  8098  mulresr  8101  addvalex  8107  pitonnlem1  8108  axi2m1  8138  axcnre  8144  mulcomli  8229  mnfnre  8265  addcomli  8367  add42i  8388  mvrraddi  8439  neg0  8468  negdii  8506  negsubdi2i  8508  crap0  9181  2t2e4  9341  3t2e6  9343  3t3e9  9344  4t2e8  9345  neg1mulneg1e1  9399  8th4div3  9406  halfpm6th  9407  iap0  9410  dfdec10  9657  deceq12i  9662  numltc  9679  decsuc  9684  decsucc  9694  nummac  9698  numma2c  9699  numadd  9700  numaddc  9701  nummul1c  9702  nummul2c  9703  decma  9704  decmac  9705  decma2c  9706  decadd  9707  decaddc  9708  decrmanc  9710  decrmac  9711  decaddci  9714  decsubi  9716  decmul1  9717  decmul1c  9718  decmul2c  9719  11multnc  9721  4t3lem  9750  6t2e12  9757  7t2e14  9762  8t2e16  9768  9t2e18  9775  9t11e99  9783  halfthird  9796  5recm6rec  9797  divfnzn  9898  xnegpnf  10106  xneg0  10109  xaddmnf1  10126  xaddmnf2  10127  mnfaddpnf  10129  iooval2  10193  dfioo2  10252  fzval2  10289  fzsuc2  10357  fztpval  10361  fz0to3un2pr  10401  fz0to4untppr  10402  fzo01  10505  fzo12sn  10506  fzo0to42pr  10509  fldiv4p1lem1div2  10609  intqfrac2  10625  intfracq  10626  xnn0nnen  10743  1tonninf  10747  neg1sqe1  10940  sq2  10941  sq3  10942  cu2  10944  i2  10946  i3  10947  binom2i  10954  sq10  11018  3dec  11020  facp1  11036  fac2  11037  fac4  11039  4bc2eq6  11080  hashp1i  11118  pr0hash2ex  11123  hashfzo  11130  hashxp  11134  zfz1isolem1  11148  elovmpowrd  11202  ccat1st1st  11265  cji  11523  cnrecnv  11531  sqrt0  11625  resqrexlemover  11631  resqrexlemcalc3  11637  absi  11680  absimle  11705  sumeq12i  11986  summodclem2a  12003  summodc  12005  sum0  12010  fsumsplitf  12030  fsum2dlemstep  12056  fsumabs  12087  fsumiun  12099  0.999...  12143  mertenslem2  12158  prodeq12i  12185  prodmodc  12200  fprod2dlemstep  12244  ege2le3  12293  eft0val  12315  cos0  12352  cos1bnd  12381  cos2bnd  12382  3dvdsdec  12487  3dvds2dec  12488  odd2np1  12495  opoe  12517  nn0o  12529  5ndvds3  12556  5ndvds6  12557  bitsfzolem  12576  m1bits  12582  gcd0val  12592  6gcd4e2  12627  nnmindc  12666  nnminle  12667  3lcm2e6woprm  12719  3lcm2e6  12793  nn0gcdsq  12833  phiprmpw  12855  phimullem  12858  pcprecl  12923  pcprendvds  12924  pcmptdvds  12979  pockthi  12992  4sqlem13m  13037  4sqlem14  13038  4sqlem17  13041  4sqlem18  13042  4sqlem19  13043  dec5nprm  13048  dec2nprm  13049  modxai  13050  modsubi  13053  numexp2x  13059  decsplit0b  13060  decsplit0  13061  decsplit  13063  karatsuba  13064  2exp5  13066  2exp7  13068  2exp8  13069  2exp11  13070  2exp16  13071  3exp3  13072  unennn  13079  ennnfonelemj0  13083  ennnfonelem0  13087  ennnfonelem1  13089  ennnfonelemhf1o  13095  ennnfonelemrn  13101  ennnfonelemdm  13102  strnfvnd  13163  slotslfn  13169  setsfun  13178  setsfun0  13179  setscom  13183  setsslid  13194  2strstr1g  13266  eqglact  13873  ecqusaddd  13886  ghmeqker  13919  dfrhm2  14230  rmodislmod  14427  cnfldadd  14638  cnfldmul  14640  expghmap  14683  fczpsrbag  14747  cnco  15012  txuni2  15047  txbas  15049  uptx  15065  txcn  15066  cnmptid  15072  cnmpt2t  15084  xmetxp  15298  cnmetdval  15320  remetdval  15338  resubmet  15347  rerestcntop  15349  rerest  15351  divcnap  15356  cnrehmeocntop  15401  dvexp  15502  plyun0  15527  plyco  15550  plycj  15552  sinhalfpilem  15582  cosneghalfpi  15589  efhalfpi  15590  cospi  15591  efipi  15592  eulerid  15593  sin2pi  15594  cos2pi  15595  ef2pi  15596  sincosq4sgn  15620  cosq14gt0  15623  tangtx  15629  sincos4thpi  15631  sincos6thpi  15633  sinkpi  15638  cosq34lt1  15641  dfrelog  15651  2logb9irr  15762  2logb9irrALT  15765  2logb9irrap  15768  mersenne  15791  perfectlem2  15794  zabsle1  15798  lgslem2  15800  lgsfcl2  15805  lgsdir2lem1  15827  lgsdir2lem2  15828  lgsdir2lem4  15830  lgsdir2lem5  15831  lgseisen  15873  2lgslem3a  15892  2lgslem3b  15893  2lgslem3c  15894  2lgslem3d  15895  2lgs2  15901  2lgsoddprmlem3a  15906  2lgsoddprmlem3b  15907  2lgsoddprmlem3c  15908  2lgsoddprmlem3d  15909  pw0ss  16004  umgrislfupgrenlem  16051  vtxdgfval  16209  clwwlknon2  16355  clwwlknon2x  16356  eupth2lembfi  16398  konigsbergvtx  16403  konigsbergiedg  16404  konigsberglem1  16409  konigsberglem2  16410  konigsberglem3  16411  ex-fl  16419  ex-exp  16421  ex-fac  16422  ex-bc  16423  ex-dvds  16424  ex-gcd  16425  bj-dfom  16629  012of  16693  2o01f  16694  pwle2  16700  nninfsellemqall  16721  isomninnlem  16742  iswomninnlem  16762  ismkvnnlem  16765  dceqnconst  16773  dcapnconst  16774  taupi  16786  gfsump1  16795