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  7371  djuf1olemr  7394  djuinr  7403  djuin  7404  djuun  7407  casefun  7425  casedm  7426  caseinj  7429  caseinl  7431  caseinr  7432  endjusym  7436  eninl  7437  eninr  7438  djudm  7445  djuinj  7446  fodjuomni  7489  fodjumkv  7500  nninfwlporlemd  7512  pm54.43  7536  exmidfodomrlemim  7553  xp2dju  7571  djucomen  7572  djuassen  7573  xpdjuen  7574  pw1nel3  7590  sucpw1nel3  7592  addpiord  7683  mulpiord  7684  dmaddpi  7692  dmmulpi  7693  recmulnqg  7758  1lt2nq  7773  halfnqq  7777  dfmq0qs  7796  dfplq0qs  7797  genpdf  7875  1prl  7922  1pru  7923  ltexprlemell  7965  ltexprlemelu  7966  recexprlemell  7989  recexprlemelu  7990  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem2  8047  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem2  8077  addsrpr  8112  mulsrpr  8113  caucvgsrlemoffres  8167  caucvgsr  8169  suplocsrlempr  8174  addcnsr  8201  mulcnsr  8202  mulresr  8205  addvalex  8211  pitonnlem1  8212  axi2m1  8242  axcnre  8248  mulcomli  8333  mnfnre  8368  addcomli  8471  add42i  8492  mvrraddi  8543  neg0  8572  negdii  8610  negsubdi2i  8612  crap0  9288  2t2e4  9459  3t2e6  9461  3t3e9  9462  4t2e8  9463  neg1mulneg1e1  9517  8th4div3  9524  halfpm6th  9525  iap0  9528  dfdec10  9780  deceq12i  9785  numltc  9802  decsuc  9807  decsucc  9817  nummac  9821  numma2c  9822  numadd  9823  numaddc  9824  nummul1c  9825  nummul2c  9826  decma  9827  decmac  9828  decma2c  9829  decadd  9830  decaddc  9831  decrmanc  9833  decrmac  9834  decaddci  9837  decsubi  9839  decmul1  9840  decmul1c  9841  decmul2c  9842  11multnc  9844  4t3lem  9873  6t2e12  9880  7t2e14  9885  8t2e16  9891  9t2e18  9898  9t11e99  9906  halfthird  9919  5recm6rec  9920  divfnzn  10021  xnegpnf  10230  xneg0  10233  xaddmnf1  10250  xaddmnf2  10251  mnfaddpnf  10253  iooval2  10317  dfioo2  10376  fzval2  10414  fzsuc2  10486  fztpval  10490  fz0to3un2pr  10530  fz0to4untppr  10531  fzo01  10634  fzo12sn  10635  fzo0to42pr  10638  fldiv4p1lem1div2  10740  intqfrac2  10756  intfracq  10757  xnn0nnen  10874  1tonninf  10878  neg1sqe1  11071  sq2  11072  sq3  11073  cu2  11075  i2  11077  i3  11078  binom2i  11085  sq10  11150  3dec  11152  facp1  11168  fac2  11169  fac4  11171  4bc2eq6  11213  hashp1i  11251  pr0hash2ex  11256  hashfzo  11263  hashxp  11267  hashfibclem  11282  zfz1isolem1  11292  elovmpowrd  11346  ccat1st1st  11409  cji  11668  cnrecnv  11676  sqrt0  11770  resqrexlemover  11776  resqrexlemcalc3  11782  absi  11825  absimle  11850  sumeq12i  12131  summodclem2a  12148  summodc  12150  sum0  12155  fsumsplitf  12175  fsum2dlemstep  12201  fsumabs  12232  fsumiun  12244  0.999...  12288  mertenslem2  12303  prodeq12i  12330  prodmodc  12345  fprod2dlemstep  12389  ege2le3  12438  eft0val  12460  cos0  12497  cos1bnd  12526  cos2bnd  12527  3dvdsdec  12632  3dvds2dec  12633  odd2np1  12640  opoe  12662  nn0o  12674  5ndvds3  12701  5ndvds6  12702  bitsfzolem  12721  m1bits  12727  gcd0val  12737  6gcd4e2  12772  nnmindc  12811  nnminle  12812  3lcm2e6woprm  12864  3lcm2e6  12938  nn0gcdsq  12978  phiprmpw  13000  phimullem  13003  pcprecl  13068  pcprendvds  13069  pcmptdvds  13124  pockthi  13137  4sqlem13m  13182  4sqlem14  13183  4sqlem17  13186  4sqlem18  13187  4sqlem19  13188  dec5nprm  13193  dec2nprm  13194  modxai  13195  modsubi  13198  numexp2x  13204  decsplit0b  13205  decsplit0  13206  decsplit  13208  karatsuba  13209  2exp5  13211  2exp7  13213  2exp8  13214  2exp11  13215  2exp16  13216  3exp3  13217  ballotfilemelo  13222  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfval0  13235  ballotfileme  13236  ballotfilemi  13243  ballotfilemsval  13252  ballotfilemrval  13261  ballotfilemrinv  13277  ballotfilemth  13281  ballotfi  13282  unennn  13288  ennnfonelemj0  13292  ennnfonelem0  13296  ennnfonelem1  13298  ennnfonelemhf1o  13304  ennnfonelemrn  13310  ennnfonelemdm  13311  strnfvnd  13372  slotslfn  13378  setsfun  13387  setsfun0  13388  setscom  13392  setsslid  13403  2strstr1g  13476  eqglact  14028  ecqusaddd  14041  ghmeqker  14074  dfrhm2  14461  rmodislmod  14688  cnfldadd  14899  cnfldmul  14901  gsumfsum  14923  expghmap  14942  asclfval  15021  fczpsrbag  15056  cnco  15322  txuni2  15357  txbas  15359  uptx  15375  txcn  15376  cnmptid  15382  cnmpt2t  15394  xmetxp  15608  cnmetdval  15630  remetdval  15648  resubmet  15657  rerestcntop  15659  rerest  15661  divcnap  15666  cnrehmeocntop  15711  dvexp  15812  plyun0  15837  plyco  15860  plycj  15862  sinhalfpilem  15892  cosneghalfpi  15899  efhalfpi  15900  cospi  15901  efipi  15902  eulerid  15903  sin2pi  15904  cos2pi  15905  ef2pi  15906  sincosq4sgn  15930  cosq14gt0  15933  tangtx  15939  sincos4thpi  15941  sincos6thpi  15943  sinkpi  15948  cosq34lt1  15951  dfrelog  15961  2logb9irr  16073  2logb9irrALT  16076  2logb9irrap  16079  log2tlbndlog2  16082  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  birthdaylem2  16088  birthdaylog2  16090  mersenne  16111  perfectlem2  16114  zabsle1  16118  lgslem2  16120  lgsfcl2  16125  lgsdir2lem1  16147  lgsdir2lem2  16148  lgsdir2lem4  16150  lgsdir2lem5  16151  lgseisen  16193  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgs2  16221  2lgsoddprmlem3a  16226  2lgsoddprmlem3b  16227  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  pw0ss  16324  umgrislfupgrenlem  16371  vtxdgfval  16529  clwwlknon2  16675  clwwlknon2x  16676  eupth2lembfi  16718  konigsbergvtx  16723  konigsbergiedg  16724  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  ex-fl  16739  ex-exp  16741  ex-fac  16742  ex-bc  16743  ex-dvds  16744  ex-gcd  16745  bj-dfom  16959  012of  17023  2o01f  17024  pwle2  17028  nninfsellemqall  17058  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102  dceqnconst  17110  dcapnconst  17111  taupi  17123