Theorem eqtri 2259

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 2249	. 2 |- ( A = B <-> A = C )
4	1, 3	mpbi 145	1 |- A = C

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2i  2260  eqtr3i  2261  eqtr4i  2262  3eqtri  2263  3eqtrri  2264  3eqtr2i  2265  cbvrab  2819  csb2  3149  cbvrabcsf  3213  difjust  3221  unjust  3223  injust  3225  dfdif3  3339  difeq12i  3345  ineqcomi  3423  inrot  3446  symdif1  3496  rabnc  3555  0in  3558  ssdifin0  3609  dfif3  3654  ifbieq2i  3664  ifbieq12i  3666  pwjust  3689  snjust  3714  dfpr2  3728  disjpr2  3773  rabsnifsb  3777  difprsn1  3854  diftpsn3  3856  difpr  3857  dfuni2  3937  intab  3999  intunsn  4008  rint0  4009  iunid  4068  viin  4072  iinrabm  4075  2iunin  4079  riin0  4084  iunxprg  4093  unopab  4210  cbvmptf  4225  cbvmpt  4226  exmid1stab  4345  unisucg  4559  op1stb  4624  orddif  4694  elxpi  4790  csbxpg  4856  relopabi  4905  inxp  4914  coeq12i  4943  dfdm3  4967  dfrn3  4969  dmun  4988  dmopab  4992  dmopab3  4994  dmxpid  5003  dmxpin  5004  rnopab  5029  rnmpt  5030  rncoss  5053  rncoeq  5056  reseq12i  5061  resundi  5076  resindi  5078  resiun1  5082  resdmdfsn  5106  resopab  5107  opabresid  5116  dfima3  5129  mptima  5138  imadisj  5149  ndmima  5164  mptcnv  5190  rnun  5196  rnuni  5199  imaundi  5200  inimass  5204  cnvxp  5206  rnxpm  5217  dminxp  5232  imainrect  5233  cnvcnv3  5237  dmpropg  5260  op1sta  5269  op2ndb  5271  op2nda  5272  resdmres  5279  mptpreima  5281  coundi  5289  coundir  5290  cocnvcnv1  5298  cores2  5300  dfdm2  5322  iotajust  5336  dfiota2  5338  funi  5409  funtp  5434  fntpg  5437  funcnvuni  5450  funcnvres  5454  imadiflem  5460  imadif  5461  imainlem  5462  imain  5463  fnresdisj  5493  mptfng  5509  fresaunres2disj  5570  resdif  5661  fv2  5690  dffv4g  5692  fveq12i  5701  nfvres  5732  0fv  5734  dfimafn2  5752  fnimapr  5763  fvmptss2  5780  fvmptg  5781  fvmpts  5783  fvmpt2  5789  mptfvex  5791  elfvmptrab  5802  fvmptndm  5804  fvopab6  5805  f1ompt  5859  dfmpt  5886  ressnop0  5896  fprg  5898  fvsnun1  5912  fsnunfv  5916  fvpr2g  5922  imauni  5967  fliftfuns  6004  cbvriota  6050  oveq123i  6099  fconstmpo  6183  resoprab  6184  mpofun  6190  rnmpo  6199  reldmmpo  6200  ov  6208  ovigg  6209  ovmpt4g  6211  ovg  6228  caov31  6279  elmpocl  6284  f1ocnvd  6292  oprabrexex2  6363  op1st  6380  op2nd  6381  f1stres  6393  f2ndres  6394  unielxp  6408  dfoprab3s  6424  dfoprab4  6426  mpompts  6434  mpofvex  6441  oprab2co  6454  df1st2  6455  df2nd2  6456  f1od2  6471  elmpom  6474  cnvimadfsn  6485  brtpos0  6523  tposoprab  6551  smores3  6564  tfrlemi14d  6604  tfr1onlemaccex  6619  tfrcllemaccex  6632  rdgisuc1  6655  rdg0  6658  frec0g  6668  df1o2  6701  df2o2  6703  oasuc  6737  omv2  6738  omsuc  6745  ecidsn  6856  qliftfuns  6893  oviec  6915  mapsncnv  6977  dfixp  6982  xpcomco  7124  xpassen  7128  ssenen  7152  undifdc  7231  unfiin  7233  fidcenumlemrks  7270  fidcenumlemr  7272  sbthlemi5  7278  sbthlemi8  7281  fi0  7309  inf00  7372  djuf1olemr  7395  djuinr  7404  djuin  7405  djuun  7408  casefun  7426  casedm  7427  caseinj  7430  caseinl  7432  caseinr  7433  endjusym  7437  eninl  7438  eninr  7439  djudm  7446  djuinj  7447  fodjuomni  7490  fodjumkv  7501  nninfwlporlemd  7513  pm54.43  7537  exmidfodomrlemim  7554  xp2dju  7572  djucomen  7573  djuassen  7574  xpdjuen  7575  pw1nel3  7591  sucpw1nel3  7593  addpiord  7684  mulpiord  7685  dmaddpi  7693  dmmulpi  7694  recmulnqg  7759  1lt2nq  7774  halfnqq  7778  dfmq0qs  7797  dfplq0qs  7798  genpdf  7876  1prl  7923  1pru  7924  ltexprlemell  7966  ltexprlemelu  7967  recexprlemell  7990  recexprlemelu  7991  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdrl  8025  cauappcvgprlem2  8028  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem2  8048  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem2  8078  addsrpr  8113  mulsrpr  8114  caucvgsrlemoffres  8168  caucvgsr  8170  suplocsrlempr  8175  addcnsr  8202  mulcnsr  8203  mulresr  8206  addvalex  8212  pitonnlem1  8213  axi2m1  8243  axcnre  8249  mulcomli  8334  mnfnre  8369  addcomli  8473  add42i  8494  mvrraddi  8545  neg0  8574  negdii  8612  negsubdi2i  8614  crap0  9291  2t2e4  9462  3t2e6  9464  3t3e9  9466  4t2e8  9467  neg1mulneg1e1  9522  8th4div3  9529  halfpm6th  9530  iap0  9533  dfdec10  9785  deceq12i  9790  numltc  9812  decsuc  9817  decsucc  9827  nummac  9831  numma2c  9832  numadd  9833  numaddc  9834  nummul1c  9835  nummul2c  9836  decma  9837  decmac  9838  decma2c  9839  decadd  9840  decaddc  9841  decrmanc  9843  decrmac  9844  decaddci  9847  decsubi  9849  decmul1  9850  decmul1c  9851  decmul2c  9852  11multnc  9854  4t3lem  9883  6t2e12  9890  7t2e14  9895  8t2e16  9901  9t2e18  9908  9t11e99  9916  halfthird  9929  5recm6rec  9930  divfnzn  10031  xnegpnf  10241  xneg0  10244  xaddmnf1  10261  xaddmnf2  10262  mnfaddpnf  10264  iooval2  10328  dfioo2  10387  fzval2  10425  fzsuc2  10497  fztpval  10501  fz0to3un2pr  10541  fz0to4untppr  10542  fzo01  10645  fzo12sn  10646  fzo0to42pr  10649  fldiv4p1lem1div2  10755  intqfrac2  10771  intfracq  10772  xnn0nnen  10889  1tonninf  10893  neg1sqe1  11086  sq2  11087  sq3  11088  cu2  11090  i2  11092  i3  11093  binom2i  11100  sq10  11166  3dec  11168  facp1  11184  fac2  11185  fac4  11187  4bc2eq6  11229  hashp1i  11267  pr0hash2ex  11272  hashfzo  11279  hashxp  11283  hashfibclem  11298  zfz1isolem1  11308  elovmpowrd  11362  ccat1st1st  11425  cji  11684  cnrecnv  11692  sqrt0  11786  resqrexlemover  11792  resqrexlemcalc3  11798  absi  11841  absimle  11867  sumeq12i  12150  summodclem2a  12167  summodc  12169  sum0  12174  fsumsplitf  12194  fsum2dlemstep  12220  fsumabs  12251  fsumiun  12263  0.999...  12307  mertenslem2  12322  prodeq12i  12349  prodmodc  12364  fprod2dlemstep  12408  ege2le3  12457  eft0val  12479  cos0  12516  cos1bnd  12545  cos2bnd  12546  3dvdsdec  12651  3dvds2dec  12652  odd2np1  12659  opoe  12681  nn0o  12693  5ndvds3  12720  5ndvds6  12721  bitsfzolem  12740  m1bits  12746  gcd0val  12756  6gcd4e2  12791  nnmindc  12830  nnminle  12831  3lcm2e6woprm  12883  3lcm2e6  12958  nn0gcdsq  12999  phiprmpw  13023  phimullem  13026  pcprecl  13091  pcprendvds  13092  pcmptdvds  13147  pockthi  13160  4sqlem13m  13205  4sqlem14  13206  4sqlem17  13209  4sqlem18  13210  4sqlem19  13211  dec5nprm  13216  dec2nprm  13217  modxai  13218  modsubi  13222  numexp2x  13228  decsplit0b  13229  decsplit0  13230  decsplit  13232  karatsuba  13233  2exp5  13235  2exp7  13237  2exp8  13238  2exp11  13239  2exp16  13240  3exp3  13241  prmlem0  13243  prmlem1  13245  5prm  13246  11prm  13252  prmlem2  13257  37prm  13258  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilemelo  13274  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfval0  13287  ballotfileme  13288  ballotfilemi  13295  ballotfilemsval  13304  ballotfilemrval  13313  ballotfilemrinv  13329  ballotfilemth  13333  ballotfi  13334  unennn  13340  ennnfonelemj0  13344  ennnfonelem0  13348  ennnfonelem1  13350  ennnfonelemhf1o  13356  ennnfonelemrn  13362  ennnfonelemdm  13363  strnfvnd  13424  slotslfn  13430  setsfun  13439  setsfun0  13440  setscom  13444  setsslid  13455  2strstr1g  13529  eqglact  14081  ecqusaddd  14094  ghmeqker  14127  dfrhm2  14545  rmodislmod  14772  cnfldadd  14983  cnfldmul  14985  gsumfsum  15007  expghmap  15026  asclfval  15105  fczpsrbag  15140  cnco  15413  txuni2  15448  txbas  15450  uptx  15466  txcn  15467  cnmptid  15473  cnmpt2t  15485  xmetxp  15699  cnmetdval  15721  remetdval  15739  resubmet  15748  rerestcntop  15750  rerest  15752  divcnap  15757  cnrehmeocntop  15802  dvexp  15903  plyun0  15928  plyco  15951  plycj  15953  sinhalfpilem  15984  cosneghalfpi  15991  efhalfpi  15992  cospi  15993  efipi  15994  eulerid  15995  sin2pi  15996  cos2pi  15997  ef2pi  15998  sincosq4sgn  16022  cosq14gt0  16025  tangtx  16031  sincos4thpi  16033  sincos6thpi  16035  sinkpi  16040  cosq34lt1  16043  dfrelog  16053  2logb9irr  16168  2logb9irrALT  16171  2logb9irrap  16174  log2tlbndlog2  16181  log2ublem2  16183  log2ublem3  16184  log2ublog2  16185  birthdaylem2  16187  birthdaylog2  16189  ppi1  16231  cht1  16232  ppiqub  16254  chtqub  16257  mersenne  16258  perfectlem2  16261  bcp1ctr  16267  bclbnd  16268  bposlem6  16277  bposlem8  16279  bposlem9  16280  zabsle1  16284  lgslem2  16286  lgsfcl2  16291  lgsdir2lem1  16313  lgsdir2lem2  16314  lgsdir2lem4  16316  lgsdir2lem5  16317  lgseisen  16359  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgs2  16387  2lgsoddprmlem3a  16392  2lgsoddprmlem3b  16393  2lgsoddprmlem3c  16394  2lgsoddprmlem3d  16395  pw0ss  16490  umgrislfupgrenlem  16537  vtxdgfval  16695  clwwlknon2  16841  clwwlknon2x  16842  eupth2lembfi  16884  konigsbergvtx  16889  konigsbergiedg  16890  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  ex-fl  16905  ex-exp  16907  ex-fac  16908  ex-bc  16909  ex-dvds  16910  ex-gcd  16911  bj-dfom  17125  012of  17189  2o01f  17190  pwle2  17194  nninfsellemqall  17224  isomninnlem  17245  iswomninnlem  17266  ismkvnnlem  17269  dceqnconst  17277  dcapnconst  17278  taupi  17290