Theorem eqtri 2255

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 2245	. 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 2216

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

This theorem is referenced by:  eqtr2i  2256  eqtr3i  2257  eqtr4i  2258  3eqtri  2259  3eqtrri  2260  3eqtr2i  2261  cbvrab  2813  csb2  3143  cbvrabcsf  3207  difjust  3215  unjust  3217  injust  3219  dfdif3  3333  difeq12i  3339  ineqcomi  3417  inrot  3440  symdif1  3490  rabnc  3545  0in  3548  ssdifin0  3595  dfif3  3640  ifbieq2i  3650  ifbieq12i  3652  pwjust  3675  snjust  3699  dfpr2  3713  disjpr2  3758  rabsnifsb  3762  difprsn1  3838  diftpsn3  3840  difpr  3841  dfuni2  3921  intab  3983  intunsn  3992  rint0  3993  iunid  4052  viin  4056  iinrabm  4059  2iunin  4063  riin0  4068  iunxprg  4077  unopab  4194  cbvmptf  4209  cbvmpt  4210  exmid1stab  4326  unisucg  4540  op1stb  4604  orddif  4674  elxpi  4770  csbxpg  4836  relopabi  4885  inxp  4894  coeq12i  4923  dfdm3  4947  dfrn3  4949  dmun  4968  dmopab  4972  dmopab3  4974  dmxpid  4983  dmxpin  4984  rnopab  5009  rnmpt  5010  rncoss  5033  rncoeq  5036  reseq12i  5041  resundi  5056  resindi  5058  resiun1  5062  resdmdfsn  5086  resopab  5087  opabresid  5096  dfima3  5109  mptima  5118  imadisj  5129  ndmima  5144  mptcnv  5170  rnun  5176  rnuni  5179  imaundi  5180  inimass  5184  cnvxp  5186  rnxpm  5197  dminxp  5212  imainrect  5213  cnvcnv3  5217  dmpropg  5240  op1sta  5249  op2ndb  5251  op2nda  5252  resdmres  5259  mptpreima  5261  coundi  5269  coundir  5270  cocnvcnv1  5278  cores2  5280  dfdm2  5302  iotajust  5316  dfiota2  5318  funi  5389  funtp  5414  fntpg  5417  funcnvuni  5430  funcnvres  5434  imadiflem  5440  imadif  5441  imainlem  5442  imain  5443  fnresdisj  5473  mptfng  5489  fresaunres2disj  5550  resdif  5641  fv2  5670  dffv4g  5672  fveq12i  5681  nfvres  5711  0fv  5713  dfimafn2  5731  fnimapr  5742  fvmptss2  5757  fvmptg  5758  fvmpts  5760  fvmpt2  5766  mptfvex  5768  elfvmptrab  5778  fvopab6  5779  f1ompt  5833  dfmpt  5860  ressnop0  5870  fprg  5872  fvsnun1  5886  fsnunfv  5890  fvpr2g  5896  imauni  5940  fliftfuns  5977  cbvriota  6023  oveq123i  6072  fconstmpo  6156  resoprab  6157  mpofun  6163  rnmpo  6172  reldmmpo  6173  ov  6181  ovigg  6182  ovmpt4g  6184  ovg  6201  caov31  6252  elmpocl  6257  f1ocnvd  6265  oprabrexex2  6336  op1st  6353  op2nd  6354  f1stres  6366  f2ndres  6367  unielxp  6381  dfoprab3s  6397  dfoprab4  6399  mpompts  6407  mpofvex  6414  oprab2co  6427  df1st2  6428  df2nd2  6429  f1od2  6444  elmpom  6447  cnvimadfsn  6458  brtpos0  6496  tposoprab  6524  smores3  6537  tfrlemi14d  6577  tfr1onlemaccex  6592  tfrcllemaccex  6605  rdgisuc1  6628  rdg0  6631  frec0g  6641  df1o2  6674  df2o2  6676  oasuc  6710  omv2  6711  omsuc  6718  ecidsn  6829  qliftfuns  6866  oviec  6888  mapsncnv  6943  dfixp  6948  xpcomco  7090  xpassen  7094  ssenen  7118  undifdc  7197  unfiin  7199  fidcenumlemrks  7236  fidcenumlemr  7238  sbthlemi5  7244  sbthlemi8  7247  fi0  7275  inf00  7335  djuf1olemr  7358  djuinr  7367  djuin  7368  djuun  7371  casefun  7389  casedm  7390  caseinj  7393  caseinl  7395  caseinr  7396  endjusym  7400  eninl  7401  eninr  7402  djudm  7409  djuinj  7410  fodjuomni  7453  fodjumkv  7464  nninfwlporlemd  7476  pm54.43  7500  exmidfodomrlemim  7517  xp2dju  7535  djucomen  7536  djuassen  7537  xpdjuen  7538  pw1nel3  7554  sucpw1nel3  7556  addpiord  7647  mulpiord  7648  dmaddpi  7656  dmmulpi  7657  recmulnqg  7722  1lt2nq  7737  halfnqq  7741  dfmq0qs  7760  dfplq0qs  7761  genpdf  7839  1prl  7886  1pru  7887  ltexprlemell  7929  ltexprlemelu  7930  recexprlemell  7953  recexprlemelu  7954  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem2  8041  addsrpr  8076  mulsrpr  8077  caucvgsrlemoffres  8131  caucvgsr  8133  suplocsrlempr  8138  addcnsr  8165  mulcnsr  8166  mulresr  8169  addvalex  8175  pitonnlem1  8176  axi2m1  8206  axcnre  8212  mulcomli  8297  mnfnre  8332  addcomli  8434  add42i  8455  mvrraddi  8506  neg0  8535  negdii  8573  negsubdi2i  8575  crap0  9249  2t2e4  9409  3t2e6  9411  3t3e9  9412  4t2e8  9413  neg1mulneg1e1  9467  8th4div3  9474  halfpm6th  9475  iap0  9478  dfdec10  9730  deceq12i  9735  numltc  9752  decsuc  9757  decsucc  9767  nummac  9771  numma2c  9772  numadd  9773  numaddc  9774  nummul1c  9775  nummul2c  9776  decma  9777  decmac  9778  decma2c  9779  decadd  9780  decaddc  9781  decrmanc  9783  decrmac  9784  decaddci  9787  decsubi  9789  decmul1  9790  decmul1c  9791  decmul2c  9792  11multnc  9794  4t3lem  9823  6t2e12  9830  7t2e14  9835  8t2e16  9841  9t2e18  9848  9t11e99  9856  halfthird  9869  5recm6rec  9870  divfnzn  9971  xnegpnf  10180  xneg0  10183  xaddmnf1  10200  xaddmnf2  10201  mnfaddpnf  10203  iooval2  10267  dfioo2  10326  fzval2  10364  fzsuc2  10435  fztpval  10439  fz0to3un2pr  10479  fz0to4untppr  10480  fzo01  10583  fzo12sn  10584  fzo0to42pr  10587  fldiv4p1lem1div2  10689  intqfrac2  10705  intfracq  10706  xnn0nnen  10823  1tonninf  10827  neg1sqe1  11020  sq2  11021  sq3  11022  cu2  11024  i2  11026  i3  11027  binom2i  11034  sq10  11099  3dec  11101  facp1  11117  fac2  11118  fac4  11120  4bc2eq6  11162  hashp1i  11200  pr0hash2ex  11205  hashfzo  11212  hashxp  11216  hashfibclem  11231  zfz1isolem1  11237  elovmpowrd  11291  ccat1st1st  11354  cji  11612  cnrecnv  11620  sqrt0  11714  resqrexlemover  11720  resqrexlemcalc3  11726  absi  11769  absimle  11794  sumeq12i  12075  summodclem2a  12092  summodc  12094  sum0  12099  fsumsplitf  12119  fsum2dlemstep  12145  fsumabs  12176  fsumiun  12188  0.999...  12232  mertenslem2  12247  prodeq12i  12274  prodmodc  12289  fprod2dlemstep  12333  ege2le3  12382  eft0val  12404  cos0  12441  cos1bnd  12470  cos2bnd  12471  3dvdsdec  12576  3dvds2dec  12577  odd2np1  12584  opoe  12606  nn0o  12618  5ndvds3  12645  5ndvds6  12646  bitsfzolem  12665  m1bits  12671  gcd0val  12681  6gcd4e2  12716  nnmindc  12755  nnminle  12756  3lcm2e6woprm  12808  3lcm2e6  12882  nn0gcdsq  12922  phiprmpw  12944  phimullem  12947  pcprecl  13012  pcprendvds  13013  pcmptdvds  13068  pockthi  13081  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  4sqlem19  13132  dec5nprm  13137  dec2nprm  13138  modxai  13139  modsubi  13142  numexp2x  13148  decsplit0b  13149  decsplit0  13150  decsplit  13152  karatsuba  13153  2exp5  13155  2exp7  13157  2exp8  13158  2exp11  13159  2exp16  13160  3exp3  13161  ballotfilemelo  13166  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfval0  13179  ballotfileme  13180  ballotfilemi  13187  ballotfilemsval  13196  ballotfilemrval  13205  ballotfilemrinv  13221  ballotfilemth  13225  ballotfi  13226  unennn  13232  ennnfonelemj0  13236  ennnfonelem0  13240  ennnfonelem1  13242  ennnfonelemhf1o  13248  ennnfonelemrn  13254  ennnfonelemdm  13255  strnfvnd  13316  slotslfn  13322  setsfun  13331  setsfun0  13332  setscom  13336  setsslid  13347  2strstr1g  13419  eqglact  13978  ecqusaddd  13991  ghmeqker  14024  gfsump1  14108  dfrhm2  14399  rmodislmod  14625  cnfldadd  14836  cnfldmul  14838  expghmap  14881  fczpsrbag  14946  cnco  15212  txuni2  15247  txbas  15249  uptx  15265  txcn  15266  cnmptid  15272  cnmpt2t  15284  xmetxp  15498  cnmetdval  15520  remetdval  15538  resubmet  15547  rerestcntop  15549  rerest  15551  divcnap  15556  cnrehmeocntop  15601  dvexp  15702  plyun0  15727  plyco  15750  plycj  15752  sinhalfpilem  15782  cosneghalfpi  15789  efhalfpi  15790  cospi  15791  efipi  15792  eulerid  15793  sin2pi  15794  cos2pi  15795  ef2pi  15796  sincosq4sgn  15820  cosq14gt0  15823  tangtx  15829  sincos4thpi  15831  sincos6thpi  15833  sinkpi  15838  cosq34lt1  15841  dfrelog  15851  2logb9irr  15962  2logb9irrALT  15965  2logb9irrap  15968  mersenne  15991  perfectlem2  15994  zabsle1  15998  lgslem2  16000  lgsfcl2  16005  lgsdir2lem1  16027  lgsdir2lem2  16028  lgsdir2lem4  16030  lgsdir2lem5  16031  lgseisen  16073  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgs2  16101  2lgsoddprmlem3a  16106  2lgsoddprmlem3b  16107  2lgsoddprmlem3c  16108  2lgsoddprmlem3d  16109  pw0ss  16204  umgrislfupgrenlem  16251  vtxdgfval  16409  clwwlknon2  16555  clwwlknon2x  16556  eupth2lembfi  16598  konigsbergvtx  16603  konigsbergiedg  16604  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  ex-fl  16619  ex-exp  16621  ex-fac  16622  ex-bc  16623  ex-dvds  16624  ex-gcd  16625  bj-dfom  16829  012of  16893  2o01f  16894  pwle2  16898  nninfsellemqall  16919  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963  dceqnconst  16972  dcapnconst  16973  taupi  16985