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

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced 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  3606  dfif3  3651  ifbieq2i  3661  ifbieq12i  3663  pwjust  3686  snjust  3710  dfpr2  3724  disjpr2  3769  rabsnifsb  3773  difprsn1  3849  diftpsn3  3851  difpr  3852  dfuni2  3932  intab  3994  intunsn  4003  rint0  4004  iunid  4063  viin  4067  iinrabm  4070  2iunin  4074  riin0  4079  iunxprg  4088  unopab  4205  cbvmptf  4220  cbvmpt  4221  exmid1stab  4340  unisucg  4554  op1stb  4619  orddif  4689  elxpi  4785  csbxpg  4851  relopabi  4900  inxp  4909  coeq12i  4938  dfdm3  4962  dfrn3  4964  dmun  4983  dmopab  4987  dmopab3  4989  dmxpid  4998  dmxpin  4999  rnopab  5024  rnmpt  5025  rncoss  5048  rncoeq  5051  reseq12i  5056  resundi  5071  resindi  5073  resiun1  5077  resdmdfsn  5101  resopab  5102  opabresid  5111  dfima3  5124  mptima  5133  imadisj  5144  ndmima  5159  mptcnv  5185  rnun  5191  rnuni  5194  imaundi  5195  inimass  5199  cnvxp  5201  rnxpm  5212  dminxp  5227  imainrect  5228  cnvcnv3  5232  dmpropg  5255  op1sta  5264  op2ndb  5266  op2nda  5267  resdmres  5274  mptpreima  5276  coundi  5284  coundir  5285  cocnvcnv1  5293  cores2  5295  dfdm2  5317  iotajust  5331  dfiota2  5333  funi  5404  funtp  5429  fntpg  5432  funcnvuni  5445  funcnvres  5449  imadiflem  5455  imadif  5456  imainlem  5457  imain  5458  fnresdisj  5488  mptfng  5504  fresaunres2disj  5565  resdif  5656  fv2  5685  dffv4g  5687  fveq12i  5696  nfvres  5726  0fv  5728  dfimafn2  5746  fnimapr  5757  fvmptss2  5774  fvmptg  5775  fvmpts  5777  fvmpt2  5783  mptfvex  5785  elfvmptrab  5795  fvopab6  5796  f1ompt  5850  dfmpt  5877  ressnop0  5887  fprg  5889  fvsnun1  5903  fsnunfv  5907  fvpr2g  5913  imauni  5957  fliftfuns  5994  cbvriota  6040  oveq123i  6089  fconstmpo  6173  resoprab  6174  mpofun  6180  rnmpo  6189  reldmmpo  6190  ov  6198  ovigg  6199  ovmpt4g  6201  ovg  6218  caov31  6269  elmpocl  6274  f1ocnvd  6282  oprabrexex2  6353  op1st  6370  op2nd  6371  f1stres  6383  f2ndres  6384  unielxp  6398  dfoprab3s  6414  dfoprab4  6416  mpompts  6424  mpofvex  6431  oprab2co  6444  df1st2  6445  df2nd2  6446  f1od2  6461  elmpom  6464  cnvimadfsn  6475  brtpos0  6513  tposoprab  6541  smores3  6554  tfrlemi14d  6594  tfr1onlemaccex  6609  tfrcllemaccex  6622  rdgisuc1  6645  rdg0  6648  frec0g  6658  df1o2  6691  df2o2  6693  oasuc  6727  omv2  6728  omsuc  6735  ecidsn  6846  qliftfuns  6883  oviec  6905  mapsncnv  6967  dfixp  6972  xpcomco  7114  xpassen  7118  ssenen  7142  undifdc  7221  unfiin  7223  fidcenumlemrks  7260  fidcenumlemr  7262  sbthlemi5  7268  sbthlemi8  7271  fi0  7299  inf00  7361  djuf1olemr  7384  djuinr  7393  djuin  7394  djuun  7397  casefun  7415  casedm  7416  caseinj  7419  caseinl  7421  caseinr  7422  endjusym  7426  eninl  7427  eninr  7428  djudm  7435  djuinj  7436  fodjuomni  7479  fodjumkv  7490  nninfwlporlemd  7502  pm54.43  7526  exmidfodomrlemim  7543  xp2dju  7561  djucomen  7562  djuassen  7563  xpdjuen  7564  pw1nel3  7580  sucpw1nel3  7582  addpiord  7673  mulpiord  7674  dmaddpi  7682  dmmulpi  7683  recmulnqg  7748  1lt2nq  7763  halfnqq  7767  dfmq0qs  7786  dfplq0qs  7787  genpdf  7865  1prl  7912  1pru  7913  ltexprlemell  7955  ltexprlemelu  7956  recexprlemell  7979  recexprlemelu  7980  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdrl  8014  cauappcvgprlem2  8017  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem2  8037  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  caucvgprprlem2  8067  addsrpr  8102  mulsrpr  8103  caucvgsrlemoffres  8157  caucvgsr  8159  suplocsrlempr  8164  addcnsr  8191  mulcnsr  8192  mulresr  8195  addvalex  8201  pitonnlem1  8202  axi2m1  8232  axcnre  8238  mulcomli  8323  mnfnre  8358  addcomli  8461  add42i  8482  mvrraddi  8533  neg0  8562  negdii  8600  negsubdi2i  8602  crap0  9278  2t2e4  9438  3t2e6  9440  3t3e9  9441  4t2e8  9442  neg1mulneg1e1  9496  8th4div3  9503  halfpm6th  9504  iap0  9507  dfdec10  9759  deceq12i  9764  numltc  9781  decsuc  9786  decsucc  9796  nummac  9800  numma2c  9801  numadd  9802  numaddc  9803  nummul1c  9804  nummul2c  9805  decma  9806  decmac  9807  decma2c  9808  decadd  9809  decaddc  9810  decrmanc  9812  decrmac  9813  decaddci  9816  decsubi  9818  decmul1  9819  decmul1c  9820  decmul2c  9821  11multnc  9823  4t3lem  9852  6t2e12  9859  7t2e14  9864  8t2e16  9870  9t2e18  9877  9t11e99  9885  halfthird  9898  5recm6rec  9899  divfnzn  10000  xnegpnf  10209  xneg0  10212  xaddmnf1  10229  xaddmnf2  10230  mnfaddpnf  10232  iooval2  10296  dfioo2  10355  fzval2  10393  fzsuc2  10464  fztpval  10468  fz0to3un2pr  10508  fz0to4untppr  10509  fzo01  10612  fzo12sn  10613  fzo0to42pr  10616  fldiv4p1lem1div2  10718  intqfrac2  10734  intfracq  10735  xnn0nnen  10852  1tonninf  10856  neg1sqe1  11049  sq2  11050  sq3  11051  cu2  11053  i2  11055  i3  11056  binom2i  11063  sq10  11128  3dec  11130  facp1  11146  fac2  11147  fac4  11149  4bc2eq6  11191  hashp1i  11229  pr0hash2ex  11234  hashfzo  11241  hashxp  11245  hashfibclem  11260  zfz1isolem1  11270  elovmpowrd  11324  ccat1st1st  11387  cji  11646  cnrecnv  11654  sqrt0  11748  resqrexlemover  11754  resqrexlemcalc3  11760  absi  11803  absimle  11828  sumeq12i  12109  summodclem2a  12126  summodc  12128  sum0  12133  fsumsplitf  12153  fsum2dlemstep  12179  fsumabs  12210  fsumiun  12222  0.999...  12266  mertenslem2  12281  prodeq12i  12308  prodmodc  12323  fprod2dlemstep  12367  ege2le3  12416  eft0val  12438  cos0  12475  cos1bnd  12504  cos2bnd  12505  3dvdsdec  12610  3dvds2dec  12611  odd2np1  12618  opoe  12640  nn0o  12652  5ndvds3  12679  5ndvds6  12680  bitsfzolem  12699  m1bits  12705  gcd0val  12715  6gcd4e2  12750  nnmindc  12789  nnminle  12790  3lcm2e6woprm  12842  3lcm2e6  12916  nn0gcdsq  12956  phiprmpw  12978  phimullem  12981  pcprecl  13046  pcprendvds  13047  pcmptdvds  13102  pockthi  13115  4sqlem13m  13160  4sqlem14  13161  4sqlem17  13164  4sqlem18  13165  4sqlem19  13166  dec5nprm  13171  dec2nprm  13172  modxai  13173  modsubi  13176  numexp2x  13182  decsplit0b  13183  decsplit0  13184  decsplit  13186  karatsuba  13187  2exp5  13189  2exp7  13191  2exp8  13192  2exp11  13193  2exp16  13194  3exp3  13195  ballotfilemelo  13200  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfval0  13213  ballotfileme  13214  ballotfilemi  13221  ballotfilemsval  13230  ballotfilemrval  13239  ballotfilemrinv  13255  ballotfilemth  13259  ballotfi  13260  unennn  13266  ennnfonelemj0  13270  ennnfonelem0  13274  ennnfonelem1  13276  ennnfonelemhf1o  13282  ennnfonelemrn  13288  ennnfonelemdm  13289  strnfvnd  13350  slotslfn  13356  setsfun  13365  setsfun0  13366  setscom  13370  setsslid  13381  2strstr1g  13453  eqglact  14005  ecqusaddd  14018  ghmeqker  14051  dfrhm2  14434  rmodislmod  14660  cnfldadd  14871  cnfldmul  14873  gsumfsum  14895  expghmap  14914  fczpsrbag  14979  cnco  15245  txuni2  15280  txbas  15282  uptx  15298  txcn  15299  cnmptid  15305  cnmpt2t  15317  xmetxp  15531  cnmetdval  15553  remetdval  15571  resubmet  15580  rerestcntop  15582  rerest  15584  divcnap  15589  cnrehmeocntop  15634  dvexp  15735  plyun0  15760  plyco  15783  plycj  15785  sinhalfpilem  15815  cosneghalfpi  15822  efhalfpi  15823  cospi  15824  efipi  15825  eulerid  15826  sin2pi  15827  cos2pi  15828  ef2pi  15829  sincosq4sgn  15853  cosq14gt0  15856  tangtx  15862  sincos4thpi  15864  sincos6thpi  15866  sinkpi  15871  cosq34lt1  15874  dfrelog  15884  2logb9irr  15996  2logb9irrALT  15999  2logb9irrap  16002  mersenne  16025  perfectlem2  16028  zabsle1  16032  lgslem2  16034  lgsfcl2  16039  lgsdir2lem1  16061  lgsdir2lem2  16062  lgsdir2lem4  16064  lgsdir2lem5  16065  lgseisen  16107  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgs2  16135  2lgsoddprmlem3a  16140  2lgsoddprmlem3b  16141  2lgsoddprmlem3c  16142  2lgsoddprmlem3d  16143  pw0ss  16238  umgrislfupgrenlem  16285  vtxdgfval  16443  clwwlknon2  16589  clwwlknon2x  16590  eupth2lembfi  16632  konigsbergvtx  16637  konigsbergiedg  16638  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  ex-fl  16653  ex-exp  16655  ex-fac  16656  ex-bc  16657  ex-dvds  16658  ex-gcd  16659  bj-dfom  16873  012of  16937  2o01f  16938  pwle2  16942  nninfsellemqall  16963  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007  dceqnconst  17015  dcapnconst  17016  taupi  17028