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  8472  add42i  8493  mvrraddi  8544  neg0  8573  negdii  8611  negsubdi2i  8613  crap0  9290  2t2e4  9461  3t2e6  9463  3t3e9  9465  4t2e8  9466  neg1mulneg1e1  9521  8th4div3  9528  halfpm6th  9529  iap0  9532  dfdec10  9784  deceq12i  9789  numltc  9811  decsuc  9816  decsucc  9826  nummac  9830  numma2c  9831  numadd  9832  numaddc  9833  nummul1c  9834  nummul2c  9835  decma  9836  decmac  9837  decma2c  9838  decadd  9839  decaddc  9840  decrmanc  9842  decrmac  9843  decaddci  9846  decsubi  9848  decmul1  9849  decmul1c  9850  decmul2c  9851  11multnc  9853  4t3lem  9882  6t2e12  9889  7t2e14  9894  8t2e16  9900  9t2e18  9907  9t11e99  9915  halfthird  9928  5recm6rec  9929  divfnzn  10030  xnegpnf  10240  xneg0  10243  xaddmnf1  10260  xaddmnf2  10261  mnfaddpnf  10263  iooval2  10327  dfioo2  10386  fzval2  10424  fzsuc2  10496  fztpval  10500  fz0to3un2pr  10540  fz0to4untppr  10541  fzo01  10644  fzo12sn  10645  fzo0to42pr  10648  fldiv4p1lem1div2  10753  intqfrac2  10769  intfracq  10770  xnn0nnen  10887  1tonninf  10891  neg1sqe1  11084  sq2  11085  sq3  11086  cu2  11088  i2  11090  i3  11091  binom2i  11098  sq10  11164  3dec  11166  facp1  11182  fac2  11183  fac4  11185  4bc2eq6  11227  hashp1i  11265  pr0hash2ex  11270  hashfzo  11277  hashxp  11281  hashfibclem  11296  zfz1isolem1  11306  elovmpowrd  11360  ccat1st1st  11423  cji  11682  cnrecnv  11690  sqrt0  11784  resqrexlemover  11790  resqrexlemcalc3  11796  absi  11839  absimle  11865  sumeq12i  12147  summodclem2a  12164  summodc  12166  sum0  12171  fsumsplitf  12191  fsum2dlemstep  12217  fsumabs  12248  fsumiun  12260  0.999...  12304  mertenslem2  12319  prodeq12i  12346  prodmodc  12361  fprod2dlemstep  12405  ege2le3  12454  eft0val  12476  cos0  12513  cos1bnd  12542  cos2bnd  12543  3dvdsdec  12648  3dvds2dec  12649  odd2np1  12656  opoe  12678  nn0o  12690  5ndvds3  12717  5ndvds6  12718  bitsfzolem  12737  m1bits  12743  gcd0val  12753  6gcd4e2  12788  nnmindc  12827  nnminle  12828  3lcm2e6woprm  12880  3lcm2e6  12955  nn0gcdsq  12996  phiprmpw  13020  phimullem  13023  pcprecl  13088  pcprendvds  13089  pcmptdvds  13144  pockthi  13157  4sqlem13m  13202  4sqlem14  13203  4sqlem17  13206  4sqlem18  13207  4sqlem19  13208  dec5nprm  13213  dec2nprm  13214  modxai  13215  modsubi  13219  numexp2x  13225  decsplit0b  13226  decsplit0  13227  decsplit  13229  karatsuba  13230  2exp5  13232  2exp7  13234  2exp8  13235  2exp11  13236  2exp16  13237  3exp3  13238  prmlem0  13240  prmlem1  13242  5prm  13243  11prm  13249  prmlem2  13254  37prm  13255  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  1259prm  13267  ballotfilemelo  13271  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfval0  13284  ballotfileme  13285  ballotfilemi  13292  ballotfilemsval  13301  ballotfilemrval  13310  ballotfilemrinv  13326  ballotfilemth  13330  ballotfi  13331  unennn  13337  ennnfonelemj0  13341  ennnfonelem0  13345  ennnfonelem1  13347  ennnfonelemhf1o  13353  ennnfonelemrn  13359  ennnfonelemdm  13360  strnfvnd  13421  slotslfn  13427  setsfun  13436  setsfun0  13437  setscom  13441  setsslid  13452  2strstr1g  13525  eqglact  14077  ecqusaddd  14090  ghmeqker  14123  dfrhm2  14510  rmodislmod  14737  cnfldadd  14948  cnfldmul  14950  gsumfsum  14972  expghmap  14991  asclfval  15070  fczpsrbag  15105  cnco  15371  txuni2  15406  txbas  15408  uptx  15424  txcn  15425  cnmptid  15431  cnmpt2t  15443  xmetxp  15657  cnmetdval  15679  remetdval  15697  resubmet  15706  rerestcntop  15708  rerest  15710  divcnap  15715  cnrehmeocntop  15760  dvexp  15861  plyun0  15886  plyco  15909  plycj  15911  sinhalfpilem  15942  cosneghalfpi  15949  efhalfpi  15950  cospi  15951  efipi  15952  eulerid  15953  sin2pi  15954  cos2pi  15955  ef2pi  15956  sincosq4sgn  15980  cosq14gt0  15983  tangtx  15989  sincos4thpi  15991  sincos6thpi  15993  sinkpi  15998  cosq34lt1  16001  dfrelog  16011  2logb9irr  16126  2logb9irrALT  16129  2logb9irrap  16132  log2tlbndlog2  16139  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  birthdaylem2  16145  birthdaylog2  16147  ppi1  16176  ppiqub  16194  mersenne  16195  perfectlem2  16198  bcp1ctr  16204  bclbnd  16205  zabsle1  16216  lgslem2  16218  lgsfcl2  16223  lgsdir2lem1  16245  lgsdir2lem2  16246  lgsdir2lem4  16248  lgsdir2lem5  16249  lgseisen  16291  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgs2  16319  2lgsoddprmlem3a  16324  2lgsoddprmlem3b  16325  2lgsoddprmlem3c  16326  2lgsoddprmlem3d  16327  pw0ss  16422  umgrislfupgrenlem  16469  vtxdgfval  16627  clwwlknon2  16773  clwwlknon2x  16774  eupth2lembfi  16816  konigsbergvtx  16821  konigsbergiedg  16822  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  ex-fl  16837  ex-exp  16839  ex-fac  16840  ex-bc  16841  ex-dvds  16842  ex-gcd  16843  bj-dfom  17057  012of  17121  2o01f  17122  pwle2  17126  nninfsellemqall  17156  isomninnlem  17177  iswomninnlem  17197  ismkvnnlem  17200  dceqnconst  17208  dcapnconst  17209  taupi  17221