Theorem eqtri 2252

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtri.1	|- A = B
eqtri.2	|- B = C

Assertion

Ref	Expression
eqtri	|- A = C

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 |- A = B
2		eqtri.2	. . 3 |- B = C
3	2	eqeq2i 2242	. 2 |- ( A = B <-> A = C )
4	1, 3	mpbi 145	1 |- A = C

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  8264  addcomli  8366  add42i  8387  mvrraddi  8438  neg0  8467  negdii  8505  negsubdi2i  8507  crap0  9180  2t2e4  9340  3t2e6  9342  3t3e9  9343  4t2e8  9344  neg1mulneg1e1  9398  8th4div3  9405  halfpm6th  9406  iap0  9409  dfdec10  9658  deceq12i  9663  numltc  9680  decsuc  9685  decsucc  9695  nummac  9699  numma2c  9700  numadd  9701  numaddc  9702  nummul1c  9703  nummul2c  9704  decma  9705  decmac  9706  decma2c  9707  decadd  9708  decaddc  9709  decrmanc  9711  decrmac  9712  decaddci  9715  decsubi  9717  decmul1  9718  decmul1c  9719  decmul2c  9720  11multnc  9722  4t3lem  9751  6t2e12  9758  7t2e14  9763  8t2e16  9769  9t2e18  9776  9t11e99  9784  halfthird  9797  5recm6rec  9798  divfnzn  9899  xnegpnf  10107  xneg0  10110  xaddmnf1  10127  xaddmnf2  10128  mnfaddpnf  10130  iooval2  10194  dfioo2  10253  fzval2  10291  fzsuc2  10359  fztpval  10363  fz0to3un2pr  10403  fz0to4untppr  10404  fzo01  10507  fzo12sn  10508  fzo0to42pr  10511  fldiv4p1lem1div2  10611  intqfrac2  10627  intfracq  10628  xnn0nnen  10745  1tonninf  10749  neg1sqe1  10942  sq2  10943  sq3  10944  cu2  10946  i2  10948  i3  10949  binom2i  10956  sq10  11020  3dec  11022  facp1  11038  fac2  11039  fac4  11041  4bc2eq6  11082  hashp1i  11120  pr0hash2ex  11125  hashfzo  11132  hashxp  11136  zfz1isolem1  11150  elovmpowrd  11204  ccat1st1st  11267  cji  11525  cnrecnv  11533  sqrt0  11627  resqrexlemover  11633  resqrexlemcalc3  11639  absi  11682  absimle  11707  sumeq12i  11988  summodclem2a  12005  summodc  12007  sum0  12012  fsumsplitf  12032  fsum2dlemstep  12058  fsumabs  12089  fsumiun  12101  0.999...  12145  mertenslem2  12160  prodeq12i  12187  prodmodc  12202  fprod2dlemstep  12246  ege2le3  12295  eft0val  12317  cos0  12354  cos1bnd  12383  cos2bnd  12384  3dvdsdec  12489  3dvds2dec  12490  odd2np1  12497  opoe  12519  nn0o  12531  5ndvds3  12558  5ndvds6  12559  bitsfzolem  12578  m1bits  12584  gcd0val  12594  6gcd4e2  12629  nnmindc  12668  nnminle  12669  3lcm2e6woprm  12721  3lcm2e6  12795  nn0gcdsq  12835  phiprmpw  12857  phimullem  12860  pcprecl  12925  pcprendvds  12926  pcmptdvds  12981  pockthi  12994  4sqlem13m  13039  4sqlem14  13040  4sqlem17  13043  4sqlem18  13044  4sqlem19  13045  dec5nprm  13050  dec2nprm  13051  modxai  13052  modsubi  13055  numexp2x  13061  decsplit0b  13062  decsplit0  13063  decsplit  13065  karatsuba  13066  2exp5  13068  2exp7  13070  2exp8  13071  2exp11  13072  2exp16  13073  3exp3  13074  unennn  13081  ennnfonelemj0  13085  ennnfonelem0  13089  ennnfonelem1  13091  ennnfonelemhf1o  13097  ennnfonelemrn  13103  ennnfonelemdm  13104  strnfvnd  13165  slotslfn  13171  setsfun  13180  setsfun0  13181  setscom  13185  setsslid  13196  2strstr1g  13268  eqglact  13875  ecqusaddd  13888  ghmeqker  13921  dfrhm2  14232  rmodislmod  14430  cnfldadd  14641  cnfldmul  14643  expghmap  14686  fczpsrbag  14750  cnco  15015  txuni2  15050  txbas  15052  uptx  15068  txcn  15069  cnmptid  15075  cnmpt2t  15087  xmetxp  15301  cnmetdval  15323  remetdval  15341  resubmet  15350  rerestcntop  15352  rerest  15354  divcnap  15359  cnrehmeocntop  15404  dvexp  15505  plyun0  15530  plyco  15553  plycj  15555  sinhalfpilem  15585  cosneghalfpi  15592  efhalfpi  15593  cospi  15594  efipi  15595  eulerid  15596  sin2pi  15597  cos2pi  15598  ef2pi  15599  sincosq4sgn  15623  cosq14gt0  15626  tangtx  15632  sincos4thpi  15634  sincos6thpi  15636  sinkpi  15641  cosq34lt1  15644  dfrelog  15654  2logb9irr  15765  2logb9irrALT  15768  2logb9irrap  15771  mersenne  15794  perfectlem2  15797  zabsle1  15801  lgslem2  15803  lgsfcl2  15808  lgsdir2lem1  15830  lgsdir2lem2  15831  lgsdir2lem4  15833  lgsdir2lem5  15834  lgseisen  15876  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgs2  15904  2lgsoddprmlem3a  15909  2lgsoddprmlem3b  15910  2lgsoddprmlem3c  15911  2lgsoddprmlem3d  15912  pw0ss  16007  umgrislfupgrenlem  16054  vtxdgfval  16212  clwwlknon2  16358  clwwlknon2x  16359  eupth2lembfi  16401  konigsbergvtx  16406  konigsbergiedg  16407  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  ex-fl  16422  ex-exp  16424  ex-fac  16425  ex-bc  16426  ex-dvds  16427  ex-gcd  16428  bj-dfom  16632  012of  16696  2o01f  16697  pwle2  16703  nninfsellemqall  16724  isomninnlem  16745  iswomninnlem  16765  ismkvnnlem  16768  dceqnconst  16776  dcapnconst  16777  taupi  16789  gfsump1  16798