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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  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  2800  csb2  3129  cbvrabcsf  3193  difjust  3201  unjust  3203  injust  3205  dfdif3  3317  difeq12i  3323  inrot  3422  symdif1  3472  rabnc  3527  0in  3530  ssdifin0  3576  dfif3  3619  ifbieq2i  3629  ifbieq12i  3631  pwjust  3653  snjust  3674  dfpr2  3688  disjpr2  3733  rabsnifsb  3737  difprsn1  3812  diftpsn3  3814  difpr  3815  dfuni2  3895  intab  3957  intunsn  3966  rint0  3967  iunid  4026  viin  4030  iinrabm  4033  2iunin  4037  riin0  4042  iunxprg  4051  unopab  4168  cbvmptf  4183  cbvmpt  4184  exmid1stab  4298  unisucg  4511  op1stb  4575  orddif  4645  elxpi  4741  csbxpg  4807  relopabi  4855  inxp  4864  coeq12i  4893  dfdm3  4917  dfrn3  4919  dmun  4938  dmopab  4942  dmopab3  4944  dmxpid  4953  dmxpin  4954  rnopab  4979  rnmpt  4980  rncoss  5003  rncoeq  5006  reseq12i  5011  resundi  5026  resindi  5028  resiun1  5032  resdmdfsn  5056  resopab  5057  opabresid  5066  dfima3  5079  mptima  5088  imadisj  5098  ndmima  5113  mptcnv  5139  rnun  5145  rnuni  5148  imaundi  5149  inimass  5153  cnvxp  5155  rnxpm  5166  dminxp  5181  imainrect  5182  cnvcnv3  5186  dmpropg  5209  op1sta  5218  op2ndb  5220  op2nda  5221  resdmres  5228  mptpreima  5230  coundi  5238  coundir  5239  cocnvcnv1  5247  cores2  5249  dfdm2  5271  iotajust  5285  dfiota2  5287  funi  5358  funtp  5383  fntpg  5386  funcnvuni  5399  funcnvres  5403  imadiflem  5409  imadif  5410  imainlem  5411  imain  5412  fnresdisj  5442  mptfng  5458  resdif  5605  fv2  5634  dffv4g  5636  fveq12i  5645  nfvres  5675  0fv  5677  dfimafn2  5695  fnimapr  5706  fvmptss2  5721  fvmptg  5722  fvmpts  5724  fvmpt2  5730  mptfvex  5732  elfvmptrab  5742  fvopab6  5743  f1ompt  5798  dfmpt  5824  ressnop0  5834  fprg  5836  fvsnun1  5850  fsnunfv  5854  fvpr2g  5860  imauni  5901  fliftfuns  5938  cbvriota  5982  oveq123i  6031  fconstmpo  6115  resoprab  6116  mpofun  6122  rnmpo  6131  reldmmpo  6132  ov  6140  ovigg  6141  ovmpt4g  6143  ovg  6160  caov31  6211  elmpocl  6216  f1ocnvd  6224  oprabrexex2  6291  op1st  6308  op2nd  6309  f1stres  6321  f2ndres  6322  unielxp  6336  dfoprab3s  6352  dfoprab4  6354  mpompts  6362  mpofvex  6369  oprab2co  6382  df1st2  6383  df2nd2  6384  f1od2  6399  elmpom  6402  brtpos0  6417  tposoprab  6445  smores3  6458  tfrlemi14d  6498  tfr1onlemaccex  6513  tfrcllemaccex  6526  rdgisuc1  6549  rdg0  6552  frec0g  6562  df1o2  6595  df2o2  6597  oasuc  6631  omv2  6632  omsuc  6639  ecidsn  6750  qliftfuns  6787  oviec  6809  mapsncnv  6863  dfixp  6868  xpcomco  7009  xpassen  7013  ssenen  7036  undifdc  7115  unfiin  7117  fidcenumlemrks  7151  fidcenumlemr  7153  sbthlemi5  7159  sbthlemi8  7162  fi0  7173  inf00  7229  djuf1olemr  7252  djuinr  7261  djuin  7262  djuun  7265  casefun  7283  casedm  7284  caseinj  7287  caseinl  7289  caseinr  7290  endjusym  7294  eninl  7295  eninr  7296  djudm  7303  djuinj  7304  fodjuomni  7347  fodjumkv  7358  nninfwlporlemd  7370  pm54.43  7394  exmidfodomrlemim  7411  xp2dju  7429  djucomen  7430  djuassen  7431  xpdjuen  7432  pw1nel3  7448  sucpw1nel3  7450  addpiord  7535  mulpiord  7536  dmaddpi  7544  dmmulpi  7545  recmulnqg  7610  1lt2nq  7625  halfnqq  7629  dfmq0qs  7648  dfplq0qs  7649  genpdf  7727  1prl  7774  1pru  7775  ltexprlemell  7817  ltexprlemelu  7818  recexprlemell  7841  recexprlemelu  7842  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdrl  7876  cauappcvgprlem2  7879  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem2  7899  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlem2  7929  addsrpr  7964  mulsrpr  7965  caucvgsrlemoffres  8019  caucvgsr  8021  suplocsrlempr  8026  addcnsr  8053  mulcnsr  8054  mulresr  8057  addvalex  8063  pitonnlem1  8064  axi2m1  8094  axcnre  8100  mulcomli  8185  mnfnre  8221  addcomli  8323  add42i  8344  mvrraddi  8395  neg0  8424  negdii  8462  negsubdi2i  8464  crap0  9137  2t2e4  9297  3t2e6  9299  3t3e9  9300  4t2e8  9301  neg1mulneg1e1  9355  8th4div3  9362  halfpm6th  9363  iap0  9366  dfdec10  9613  deceq12i  9618  numltc  9635  decsuc  9640  decsucc  9650  nummac  9654  numma2c  9655  numadd  9656  numaddc  9657  nummul1c  9658  nummul2c  9659  decma  9660  decmac  9661  decma2c  9662  decadd  9663  decaddc  9664  decrmanc  9666  decrmac  9667  decaddci  9670  decsubi  9672  decmul1  9673  decmul1c  9674  decmul2c  9675  11multnc  9677  4t3lem  9706  6t2e12  9713  7t2e14  9718  8t2e16  9724  9t2e18  9731  9t11e99  9739  halfthird  9752  5recm6rec  9753  divfnzn  9854  xnegpnf  10062  xneg0  10065  xaddmnf1  10082  xaddmnf2  10083  mnfaddpnf  10085  iooval2  10149  dfioo2  10208  fzval2  10245  fzsuc2  10313  fztpval  10317  fz0to3un2pr  10357  fz0to4untppr  10358  fzo01  10460  fzo12sn  10461  fzo0to42pr  10464  fldiv4p1lem1div2  10564  intqfrac2  10580  intfracq  10581  xnn0nnen  10698  1tonninf  10702  neg1sqe1  10895  sq2  10896  sq3  10897  cu2  10899  i2  10901  i3  10902  binom2i  10909  sq10  10973  3dec  10975  facp1  10991  fac2  10992  fac4  10994  4bc2eq6  11035  hashp1i  11073  pr0hash2ex  11078  hashfzo  11085  hashxp  11089  zfz1isolem1  11103  elovmpowrd  11154  ccat1st1st  11217  cji  11462  cnrecnv  11470  sqrt0  11564  resqrexlemover  11570  resqrexlemcalc3  11576  absi  11619  absimle  11644  sumeq12i  11925  summodclem2a  11941  summodc  11943  sum0  11948  fsumsplitf  11968  fsum2dlemstep  11994  fsumabs  12025  fsumiun  12037  0.999...  12081  mertenslem2  12096  prodeq12i  12123  prodmodc  12138  fprod2dlemstep  12182  ege2le3  12231  eft0val  12253  cos0  12290  cos1bnd  12319  cos2bnd  12320  3dvdsdec  12425  3dvds2dec  12426  odd2np1  12433  opoe  12455  nn0o  12467  5ndvds3  12494  5ndvds6  12495  bitsfzolem  12514  m1bits  12520  gcd0val  12530  6gcd4e2  12565  nnmindc  12604  nnminle  12605  3lcm2e6woprm  12657  3lcm2e6  12731  nn0gcdsq  12771  phiprmpw  12793  phimullem  12796  pcprecl  12861  pcprendvds  12862  pcmptdvds  12917  pockthi  12930  4sqlem13m  12975  4sqlem14  12976  4sqlem17  12979  4sqlem18  12980  4sqlem19  12981  dec5nprm  12986  dec2nprm  12987  modxai  12988  modsubi  12991  numexp2x  12997  decsplit0b  12998  decsplit0  12999  decsplit  13001  karatsuba  13002  2exp5  13004  2exp7  13006  2exp8  13007  2exp11  13008  2exp16  13009  3exp3  13010  unennn  13017  ennnfonelemj0  13021  ennnfonelem0  13025  ennnfonelem1  13027  ennnfonelemhf1o  13033  ennnfonelemrn  13039  ennnfonelemdm  13040  strnfvnd  13101  slotslfn  13107  setsfun  13116  setsfun0  13117  setscom  13121  setsslid  13132  2strstr1g  13204  eqglact  13811  ecqusaddd  13824  ghmeqker  13857  dfrhm2  14167  rmodislmod  14364  cnfldadd  14575  cnfldmul  14577  expghmap  14620  fczpsrbag  14684  cnco  14944  txuni2  14979  txbas  14981  uptx  14997  txcn  14998  cnmptid  15004  cnmpt2t  15016  xmetxp  15230  cnmetdval  15252  remetdval  15270  resubmet  15279  rerestcntop  15281  rerest  15283  divcnap  15288  cnrehmeocntop  15333  dvexp  15434  plyun0  15459  plyco  15482  plycj  15484  sinhalfpilem  15514  cosneghalfpi  15521  efhalfpi  15522  cospi  15523  efipi  15524  eulerid  15525  sin2pi  15526  cos2pi  15527  ef2pi  15528  sincosq4sgn  15552  cosq14gt0  15555  tangtx  15561  sincos4thpi  15563  sincos6thpi  15565  sinkpi  15570  cosq34lt1  15573  dfrelog  15583  2logb9irr  15694  2logb9irrALT  15697  2logb9irrap  15700  mersenne  15720  perfectlem2  15723  zabsle1  15727  lgslem2  15729  lgsfcl2  15734  lgsdir2lem1  15756  lgsdir2lem2  15757  lgsdir2lem4  15759  lgsdir2lem5  15760  lgseisen  15802  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgs2  15830  2lgsoddprmlem3a  15835  2lgsoddprmlem3b  15836  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838  pw0ss  15933  umgrislfupgrenlem  15980  vtxdgfval  16138  clwwlknon2  16284  clwwlknon2x  16285  ex-fl  16321  ex-exp  16323  ex-fac  16324  ex-bc  16325  ex-dvds  16326  ex-gcd  16327  bj-dfom  16528  012of  16592  2o01f  16593  pwle2  16599  nninfsellemqall  16617  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656  dceqnconst  16664  dcapnconst  16665  taupi  16677