Theorem eqtri 2253

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 2243	. 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 2214

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

This theorem is referenced by:  eqtr2i  2254  eqtr3i  2255  eqtr4i  2256  3eqtri  2257  3eqtrri  2258  3eqtr2i  2259  cbvrab  2811  csb2  3140  cbvrabcsf  3204  difjust  3212  unjust  3214  injust  3216  dfdif3  3329  difeq12i  3335  ineqcomi  3413  inrot  3436  symdif1  3486  rabnc  3541  0in  3544  ssdifin0  3591  dfif3  3636  ifbieq2i  3646  ifbieq12i  3648  pwjust  3670  snjust  3694  dfpr2  3708  disjpr2  3753  rabsnifsb  3757  difprsn1  3833  diftpsn3  3835  difpr  3836  dfuni2  3916  intab  3978  intunsn  3987  rint0  3988  iunid  4047  viin  4051  iinrabm  4054  2iunin  4058  riin0  4063  iunxprg  4072  unopab  4189  cbvmptf  4204  cbvmpt  4205  exmid1stab  4321  unisucg  4535  op1stb  4599  orddif  4669  elxpi  4765  csbxpg  4831  relopabi  4880  inxp  4889  coeq12i  4918  dfdm3  4942  dfrn3  4944  dmun  4963  dmopab  4967  dmopab3  4969  dmxpid  4978  dmxpin  4979  rnopab  5004  rnmpt  5005  rncoss  5028  rncoeq  5031  reseq12i  5036  resundi  5051  resindi  5053  resiun1  5057  resdmdfsn  5081  resopab  5082  opabresid  5091  dfima3  5104  mptima  5113  imadisj  5124  ndmima  5139  mptcnv  5165  rnun  5171  rnuni  5174  imaundi  5175  inimass  5179  cnvxp  5181  rnxpm  5192  dminxp  5207  imainrect  5208  cnvcnv3  5212  dmpropg  5235  op1sta  5244  op2ndb  5246  op2nda  5247  resdmres  5254  mptpreima  5256  coundi  5264  coundir  5265  cocnvcnv1  5273  cores2  5275  dfdm2  5297  iotajust  5311  dfiota2  5313  funi  5384  funtp  5409  fntpg  5412  funcnvuni  5425  funcnvres  5429  imadiflem  5435  imadif  5436  imainlem  5437  imain  5438  fnresdisj  5468  mptfng  5484  fresaunres2disj  5545  resdif  5636  fv2  5665  dffv4g  5667  fveq12i  5676  nfvres  5706  0fv  5708  dfimafn2  5726  fnimapr  5737  fvmptss2  5752  fvmptg  5753  fvmpts  5755  fvmpt2  5761  mptfvex  5763  elfvmptrab  5773  fvopab6  5774  f1ompt  5828  dfmpt  5855  ressnop0  5865  fprg  5867  fvsnun1  5881  fsnunfv  5885  fvpr2g  5891  imauni  5934  fliftfuns  5971  cbvriota  6015  oveq123i  6064  fconstmpo  6148  resoprab  6149  mpofun  6155  rnmpo  6164  reldmmpo  6165  ov  6173  ovigg  6174  ovmpt4g  6176  ovg  6193  caov31  6244  elmpocl  6249  f1ocnvd  6257  oprabrexex2  6323  op1st  6340  op2nd  6341  f1stres  6353  f2ndres  6354  unielxp  6368  dfoprab3s  6384  dfoprab4  6386  mpompts  6394  mpofvex  6401  oprab2co  6414  df1st2  6415  df2nd2  6416  f1od2  6431  elmpom  6434  cnvimadfsn  6445  brtpos0  6483  tposoprab  6511  smores3  6524  tfrlemi14d  6564  tfr1onlemaccex  6579  tfrcllemaccex  6592  rdgisuc1  6615  rdg0  6618  frec0g  6628  df1o2  6661  df2o2  6663  oasuc  6697  omv2  6698  omsuc  6705  ecidsn  6816  qliftfuns  6853  oviec  6875  mapsncnv  6930  dfixp  6935  xpcomco  7077  xpassen  7081  ssenen  7105  undifdc  7184  unfiin  7186  fidcenumlemrks  7223  fidcenumlemr  7225  sbthlemi5  7231  sbthlemi8  7234  fi0  7262  inf00  7322  djuf1olemr  7345  djuinr  7354  djuin  7355  djuun  7358  casefun  7376  casedm  7377  caseinj  7380  caseinl  7382  caseinr  7383  endjusym  7387  eninl  7388  eninr  7389  djudm  7396  djuinj  7397  fodjuomni  7440  fodjumkv  7451  nninfwlporlemd  7463  pm54.43  7487  exmidfodomrlemim  7504  xp2dju  7522  djucomen  7523  djuassen  7524  xpdjuen  7525  pw1nel3  7541  sucpw1nel3  7543  addpiord  7631  mulpiord  7632  dmaddpi  7640  dmmulpi  7641  recmulnqg  7706  1lt2nq  7721  halfnqq  7725  dfmq0qs  7744  dfplq0qs  7745  genpdf  7823  1prl  7870  1pru  7871  ltexprlemell  7913  ltexprlemelu  7914  recexprlemell  7937  recexprlemelu  7938  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemopu  7963  cauappcvgprlemupu  7964  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdrl  7972  cauappcvgprlem2  7975  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemopu  7986  caucvgprlemupu  7987  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem2  7995  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  caucvgprprlem2  8025  addsrpr  8060  mulsrpr  8061  caucvgsrlemoffres  8115  caucvgsr  8117  suplocsrlempr  8122  addcnsr  8149  mulcnsr  8150  mulresr  8153  addvalex  8159  pitonnlem1  8160  axi2m1  8190  axcnre  8196  mulcomli  8281  mnfnre  8316  addcomli  8418  add42i  8439  mvrraddi  8490  neg0  8519  negdii  8557  negsubdi2i  8559  crap0  9232  2t2e4  9392  3t2e6  9394  3t3e9  9395  4t2e8  9396  neg1mulneg1e1  9450  8th4div3  9457  halfpm6th  9458  iap0  9461  dfdec10  9712  deceq12i  9717  numltc  9734  decsuc  9739  decsucc  9749  nummac  9753  numma2c  9754  numadd  9755  numaddc  9756  nummul1c  9757  nummul2c  9758  decma  9759  decmac  9760  decma2c  9761  decadd  9762  decaddc  9763  decrmanc  9765  decrmac  9766  decaddci  9769  decsubi  9771  decmul1  9772  decmul1c  9773  decmul2c  9774  11multnc  9776  4t3lem  9805  6t2e12  9812  7t2e14  9817  8t2e16  9823  9t2e18  9830  9t11e99  9838  halfthird  9851  5recm6rec  9852  divfnzn  9953  xnegpnf  10161  xneg0  10164  xaddmnf1  10181  xaddmnf2  10182  mnfaddpnf  10184  iooval2  10248  dfioo2  10307  fzval2  10345  fzsuc2  10413  fztpval  10417  fz0to3un2pr  10457  fz0to4untppr  10458  fzo01  10561  fzo12sn  10562  fzo0to42pr  10565  fldiv4p1lem1div2  10665  intqfrac2  10681  intfracq  10682  xnn0nnen  10799  1tonninf  10803  neg1sqe1  10996  sq2  10997  sq3  10998  cu2  11000  i2  11002  i3  11003  binom2i  11010  sq10  11074  3dec  11076  facp1  11092  fac2  11093  fac4  11095  4bc2eq6  11137  hashp1i  11175  pr0hash2ex  11180  hashfzo  11187  hashxp  11191  hashfibclem  11206  zfz1isolem1  11212  elovmpowrd  11266  ccat1st1st  11329  cji  11587  cnrecnv  11595  sqrt0  11689  resqrexlemover  11695  resqrexlemcalc3  11701  absi  11744  absimle  11769  sumeq12i  12050  summodclem2a  12067  summodc  12069  sum0  12074  fsumsplitf  12094  fsum2dlemstep  12120  fsumabs  12151  fsumiun  12163  0.999...  12207  mertenslem2  12222  prodeq12i  12249  prodmodc  12264  fprod2dlemstep  12308  ege2le3  12357  eft0val  12379  cos0  12416  cos1bnd  12445  cos2bnd  12446  3dvdsdec  12551  3dvds2dec  12552  odd2np1  12559  opoe  12581  nn0o  12593  5ndvds3  12620  5ndvds6  12621  bitsfzolem  12640  m1bits  12646  gcd0val  12656  6gcd4e2  12691  nnmindc  12730  nnminle  12731  3lcm2e6woprm  12783  3lcm2e6  12857  nn0gcdsq  12897  phiprmpw  12919  phimullem  12922  pcprecl  12987  pcprendvds  12988  pcmptdvds  13043  pockthi  13056  4sqlem13m  13101  4sqlem14  13102  4sqlem17  13105  4sqlem18  13106  4sqlem19  13107  dec5nprm  13112  dec2nprm  13113  modxai  13114  modsubi  13117  numexp2x  13123  decsplit0b  13124  decsplit0  13125  decsplit  13127  karatsuba  13128  2exp5  13130  2exp7  13132  2exp8  13133  2exp11  13134  2exp16  13135  3exp3  13136  ballotfilemelo  13141  ballotfilem2  13142  unennn  13148  ennnfonelemj0  13152  ennnfonelem0  13156  ennnfonelem1  13158  ennnfonelemhf1o  13164  ennnfonelemrn  13170  ennnfonelemdm  13171  strnfvnd  13232  slotslfn  13238  setsfun  13247  setsfun0  13248  setscom  13252  setsslid  13263  2strstr1g  13335  eqglact  13942  ecqusaddd  13955  ghmeqker  13988  dfrhm2  14299  rmodislmod  14499  cnfldadd  14710  cnfldmul  14712  expghmap  14755  fczpsrbag  14820  cnco  15086  txuni2  15121  txbas  15123  uptx  15139  txcn  15140  cnmptid  15146  cnmpt2t  15158  xmetxp  15372  cnmetdval  15394  remetdval  15412  resubmet  15421  rerestcntop  15423  rerest  15425  divcnap  15430  cnrehmeocntop  15475  dvexp  15576  plyun0  15601  plyco  15624  plycj  15626  sinhalfpilem  15656  cosneghalfpi  15663  efhalfpi  15664  cospi  15665  efipi  15666  eulerid  15667  sin2pi  15668  cos2pi  15669  ef2pi  15670  sincosq4sgn  15694  cosq14gt0  15697  tangtx  15703  sincos4thpi  15705  sincos6thpi  15707  sinkpi  15712  cosq34lt1  15715  dfrelog  15725  2logb9irr  15836  2logb9irrALT  15839  2logb9irrap  15842  mersenne  15865  perfectlem2  15868  zabsle1  15872  lgslem2  15874  lgsfcl2  15879  lgsdir2lem1  15901  lgsdir2lem2  15902  lgsdir2lem4  15904  lgsdir2lem5  15905  lgseisen  15947  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgs2  15975  2lgsoddprmlem3a  15980  2lgsoddprmlem3b  15981  2lgsoddprmlem3c  15982  2lgsoddprmlem3d  15983  pw0ss  16078  umgrislfupgrenlem  16125  vtxdgfval  16283  clwwlknon2  16429  clwwlknon2x  16430  eupth2lembfi  16472  konigsbergvtx  16477  konigsbergiedg  16478  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  ex-fl  16493  ex-exp  16495  ex-fac  16496  ex-bc  16497  ex-dvds  16498  ex-gcd  16499  bj-dfom  16703  012of  16767  2o01f  16768  pwle2  16772  nninfsellemqall  16793  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837  dceqnconst  16846  dcapnconst  16847  taupi  16859  gfsump1  16868