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  5825  ressnop0  5835  fprg  5837  fvsnun1  5851  fsnunfv  5855  fvpr2g  5861  imauni  5902  fliftfuns  5939  cbvriota  5983  oveq123i  6032  fconstmpo  6116  resoprab  6117  mpofun  6123  rnmpo  6132  reldmmpo  6133  ov  6141  ovigg  6142  ovmpt4g  6144  ovg  6161  caov31  6212  elmpocl  6217  f1ocnvd  6225  oprabrexex2  6292  op1st  6309  op2nd  6310  f1stres  6322  f2ndres  6323  unielxp  6337  dfoprab3s  6353  dfoprab4  6355  mpompts  6363  mpofvex  6370  oprab2co  6383  df1st2  6384  df2nd2  6385  f1od2  6400  elmpom  6403  brtpos0  6418  tposoprab  6446  smores3  6459  tfrlemi14d  6499  tfr1onlemaccex  6514  tfrcllemaccex  6527  rdgisuc1  6550  rdg0  6553  frec0g  6563  df1o2  6596  df2o2  6598  oasuc  6632  omv2  6633  omsuc  6640  ecidsn  6751  qliftfuns  6788  oviec  6810  mapsncnv  6864  dfixp  6869  xpcomco  7010  xpassen  7014  ssenen  7037  undifdc  7116  unfiin  7118  fidcenumlemrks  7152  fidcenumlemr  7154  sbthlemi5  7160  sbthlemi8  7163  fi0  7174  inf00  7230  djuf1olemr  7253  djuinr  7262  djuin  7263  djuun  7266  casefun  7284  casedm  7285  caseinj  7288  caseinl  7290  caseinr  7291  endjusym  7295  eninl  7296  eninr  7297  djudm  7304  djuinj  7305  fodjuomni  7348  fodjumkv  7359  nninfwlporlemd  7371  pm54.43  7395  exmidfodomrlemim  7412  xp2dju  7430  djucomen  7431  djuassen  7432  xpdjuen  7433  pw1nel3  7449  sucpw1nel3  7451  addpiord  7536  mulpiord  7537  dmaddpi  7545  dmmulpi  7546  recmulnqg  7611  1lt2nq  7626  halfnqq  7630  dfmq0qs  7649  dfplq0qs  7650  genpdf  7728  1prl  7775  1pru  7776  ltexprlemell  7818  ltexprlemelu  7819  recexprlemell  7842  recexprlemelu  7843  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem2  7900  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem2  7930  addsrpr  7965  mulsrpr  7966  caucvgsrlemoffres  8020  caucvgsr  8022  suplocsrlempr  8027  addcnsr  8054  mulcnsr  8055  mulresr  8058  addvalex  8064  pitonnlem1  8065  axi2m1  8095  axcnre  8101  mulcomli  8186  mnfnre  8222  addcomli  8324  add42i  8345  mvrraddi  8396  neg0  8425  negdii  8463  negsubdi2i  8465  crap0  9138  2t2e4  9298  3t2e6  9300  3t3e9  9301  4t2e8  9302  neg1mulneg1e1  9356  8th4div3  9363  halfpm6th  9364  iap0  9367  dfdec10  9614  deceq12i  9619  numltc  9636  decsuc  9641  decsucc  9651  nummac  9655  numma2c  9656  numadd  9657  numaddc  9658  nummul1c  9659  nummul2c  9660  decma  9661  decmac  9662  decma2c  9663  decadd  9664  decaddc  9665  decrmanc  9667  decrmac  9668  decaddci  9671  decsubi  9673  decmul1  9674  decmul1c  9675  decmul2c  9676  11multnc  9678  4t3lem  9707  6t2e12  9714  7t2e14  9719  8t2e16  9725  9t2e18  9732  9t11e99  9740  halfthird  9753  5recm6rec  9754  divfnzn  9855  xnegpnf  10063  xneg0  10066  xaddmnf1  10083  xaddmnf2  10084  mnfaddpnf  10086  iooval2  10150  dfioo2  10209  fzval2  10246  fzsuc2  10314  fztpval  10318  fz0to3un2pr  10358  fz0to4untppr  10359  fzo01  10462  fzo12sn  10463  fzo0to42pr  10466  fldiv4p1lem1div2  10566  intqfrac2  10582  intfracq  10583  xnn0nnen  10700  1tonninf  10704  neg1sqe1  10897  sq2  10898  sq3  10899  cu2  10901  i2  10903  i3  10904  binom2i  10911  sq10  10975  3dec  10977  facp1  10993  fac2  10994  fac4  10996  4bc2eq6  11037  hashp1i  11075  pr0hash2ex  11080  hashfzo  11087  hashxp  11091  zfz1isolem1  11105  elovmpowrd  11159  ccat1st1st  11222  cji  11480  cnrecnv  11488  sqrt0  11582  resqrexlemover  11588  resqrexlemcalc3  11594  absi  11637  absimle  11662  sumeq12i  11943  summodclem2a  11960  summodc  11962  sum0  11967  fsumsplitf  11987  fsum2dlemstep  12013  fsumabs  12044  fsumiun  12056  0.999...  12100  mertenslem2  12115  prodeq12i  12142  prodmodc  12157  fprod2dlemstep  12201  ege2le3  12250  eft0val  12272  cos0  12309  cos1bnd  12338  cos2bnd  12339  3dvdsdec  12444  3dvds2dec  12445  odd2np1  12452  opoe  12474  nn0o  12486  5ndvds3  12513  5ndvds6  12514  bitsfzolem  12533  m1bits  12539  gcd0val  12549  6gcd4e2  12584  nnmindc  12623  nnminle  12624  3lcm2e6woprm  12676  3lcm2e6  12750  nn0gcdsq  12790  phiprmpw  12812  phimullem  12815  pcprecl  12880  pcprendvds  12881  pcmptdvds  12936  pockthi  12949  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  4sqlem18  12999  4sqlem19  13000  dec5nprm  13005  dec2nprm  13006  modxai  13007  modsubi  13010  numexp2x  13016  decsplit0b  13017  decsplit0  13018  decsplit  13020  karatsuba  13021  2exp5  13023  2exp7  13025  2exp8  13026  2exp11  13027  2exp16  13028  3exp3  13029  unennn  13036  ennnfonelemj0  13040  ennnfonelem0  13044  ennnfonelem1  13046  ennnfonelemhf1o  13052  ennnfonelemrn  13058  ennnfonelemdm  13059  strnfvnd  13120  slotslfn  13126  setsfun  13135  setsfun0  13136  setscom  13140  setsslid  13151  2strstr1g  13223  eqglact  13830  ecqusaddd  13843  ghmeqker  13876  dfrhm2  14187  rmodislmod  14384  cnfldadd  14595  cnfldmul  14597  expghmap  14640  fczpsrbag  14704  cnco  14964  txuni2  14999  txbas  15001  uptx  15017  txcn  15018  cnmptid  15024  cnmpt2t  15036  xmetxp  15250  cnmetdval  15272  remetdval  15290  resubmet  15299  rerestcntop  15301  rerest  15303  divcnap  15308  cnrehmeocntop  15353  dvexp  15454  plyun0  15479  plyco  15502  plycj  15504  sinhalfpilem  15534  cosneghalfpi  15541  efhalfpi  15542  cospi  15543  efipi  15544  eulerid  15545  sin2pi  15546  cos2pi  15547  ef2pi  15548  sincosq4sgn  15572  cosq14gt0  15575  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  sinkpi  15590  cosq34lt1  15593  dfrelog  15603  2logb9irr  15714  2logb9irrALT  15717  2logb9irrap  15720  mersenne  15740  perfectlem2  15743  zabsle1  15747  lgslem2  15749  lgsfcl2  15754  lgsdir2lem1  15776  lgsdir2lem2  15777  lgsdir2lem4  15779  lgsdir2lem5  15780  lgseisen  15822  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgs2  15850  2lgsoddprmlem3a  15855  2lgsoddprmlem3b  15856  2lgsoddprmlem3c  15857  2lgsoddprmlem3d  15858  pw0ss  15953  umgrislfupgrenlem  16000  vtxdgfval  16158  clwwlknon2  16304  clwwlknon2x  16305  eupth2lembfi  16347  konigsbergvtx  16352  konigsbergiedg  16353  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  ex-fl  16368  ex-exp  16370  ex-fac  16371  ex-bc  16372  ex-dvds  16373  ex-gcd  16374  bj-dfom  16579  012of  16643  2o01f  16644  pwle2  16650  nninfsellemqall  16668  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708  dceqnconst  16716  dcapnconst  16717  taupi  16729  gfsump1  16738