Theorem eqtri 2115

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

Syntax hints:   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088

This theorem is referenced by:  eqtr2i  2116  eqtr3i  2117  eqtr4i  2118  3eqtri  2119  3eqtrri  2120  3eqtr2i  2121  cbvrab  2631  csb2  2949  cbvrabcsf  3007  difjust  3014  unjust  3016  injust  3018  dfdif3  3125  difeq12i  3131  inrot  3230  symdif1  3280  rabnc  3334  0in  3337  ssdifin0  3383  dfif3  3426  ifbieq2i  3434  ifbieq12i  3436  pwjust  3450  snjust  3471  dfpr2  3485  disjpr2  3526  difprsn1  3598  diftpsn3  3600  difpr  3601  dfuni2  3677  intab  3739  intunsn  3748  rint0  3749  iunid  3807  viin  3811  iinrabm  3814  2iunin  3818  riin0  3823  unopab  3939  cbvmptf  3954  cbvmpt  3955  unisucg  4265  op1stb  4328  orddif  4391  elxpi  4483  csbxpg  4548  relopabi  4593  inxp  4601  coeq12i  4630  dfdm3  4654  dfrn3  4656  dmun  4674  dmopab  4678  dmopab3  4680  dmxpid  4688  dmxpin  4689  rnopab  4714  rnmpt  4715  rncoss  4735  rncoeq  4738  reseq12i  4743  resundi  4758  resindi  4760  resiun1  4764  resdmdfsn  4788  resopab  4789  mptresid  4799  dfima3  4810  imadisj  4827  ndmima  4842  mptcnv  4867  rnun  4873  rnuni  4876  imaundi  4877  inimass  4881  cnvxp  4883  rnxpm  4894  dminxp  4909  imainrect  4910  cnvcnv3  4914  dmpropg  4937  op1sta  4946  op2ndb  4948  op2nda  4949  resdmres  4956  mptpreima  4958  coundi  4966  coundir  4967  cocnvcnv1  4975  cores2  4977  dfdm2  4999  iotajust  5013  dfiota2  5015  funi  5080  funtp  5101  fntpg  5104  funcnvuni  5117  funcnvres  5121  imadiflem  5127  imadif  5128  imainlem  5129  imain  5130  fnresdisj  5158  mptfng  5173  resdif  5310  fv2  5335  dffv4g  5337  fveq12i  5346  nfvres  5372  0fv  5374  dfimafn2  5389  fnimapr  5399  fvmptss2  5414  fvmptg  5415  fvmpts  5417  fvmpt2  5422  mptfvex  5424  elfvmptrab  5434  fvopab6  5435  f1ompt  5489  dfmpt  5513  ressnop0  5517  fprg  5519  fvsnun1  5533  fsnunfv  5537  fvpr2g  5543  imauni  5578  fliftfuns  5615  cbvriota  5656  oveq123i  5704  resoprab  5779  mpt2fun  5785  rnmpt2  5793  reldmmpt2  5794  ov  5802  ovigg  5803  ovmpt4g  5805  ovg  5821  caov31  5872  elmpt2cl  5880  f1ocnvd  5884  oprabrexex2  5939  op1st  5955  op2nd  5956  f1stres  5968  f2ndres  5969  unielxp  5982  dfoprab3s  5998  dfoprab4  6000  mpt2mpts  6006  mpt2fvex  6011  oprab2co  6021  df1st2  6022  df2nd2  6023  f1od2  6038  brtpos0  6055  tposoprab  6083  smores3  6096  tfrlemi14d  6136  tfr1onlemaccex  6151  tfrcllemaccex  6164  rdgisuc1  6187  rdg0  6190  frec0g  6200  df1o2  6232  df2o2  6234  oasuc  6265  omv2  6266  omsuc  6273  ecidsn  6379  qliftfuns  6416  oviec  6438  mapsncnv  6492  dfixp  6497  xpcomco  6622  xpassen  6626  ssenen  6647  undifdc  6714  unfiin  6716  fidcenumlemrks  6742  fidcenumlemr  6744  sbthlemi5  6750  sbthlemi8  6753  inf00  6806  djuf1olemr  6826  djuinr  6835  casefun  6856  casedm  6857  caseinj  6860  caseinl  6862  djudm  6867  djuinj  6868  fodjuomni  6892  fodjumkv  6903  pm54.43  6915  exmidfodomrlemim  6924  addpiord  6972  mulpiord  6973  dmaddpi  6981  dmmulpi  6982  recmulnqg  7047  1lt2nq  7062  halfnqq  7066  dfmq0qs  7085  dfplq0qs  7086  genpdf  7164  1prl  7211  1pru  7212  ltexprlemell  7254  ltexprlemelu  7255  recexprlemell  7278  recexprlemelu  7279  cauappcvgprlemm  7301  cauappcvgprlemopl  7302  cauappcvgprlemlol  7303  cauappcvgprlemopu  7304  cauappcvgprlemupu  7305  cauappcvgprlemdisj  7307  cauappcvgprlemloc  7308  cauappcvgprlemladdfu  7310  cauappcvgprlemladdfl  7311  cauappcvgprlemladdrl  7313  cauappcvgprlem2  7316  caucvgprlemm  7324  caucvgprlemopl  7325  caucvgprlemlol  7326  caucvgprlemopu  7327  caucvgprlemupu  7328  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemcl  7332  caucvgprlemladdfu  7333  caucvgprlemladdrl  7334  caucvgprlem2  7336  caucvgprprlemell  7341  caucvgprprlemelu  7342  caucvgprprlemml  7350  caucvgprprlemmu  7351  caucvgprprlemclphr  7361  caucvgprprlemexbt  7362  caucvgprprlem2  7366  addsrpr  7388  mulsrpr  7389  caucvgsrlemoffres  7442  caucvgsr  7444  addcnsr  7468  mulcnsr  7469  mulresr  7472  addvalex  7478  pitonnlem1  7479  axi2m1  7507  axcnre  7513  mulcomli  7592  mnfnre  7627  addcomli  7724  add42i  7745  mvrraddi  7796  neg0  7825  negdii  7863  negsubdi2i  7865  crap0  8516  2t2e4  8668  3t2e6  8670  3t3e9  8671  4t2e8  8672  neg1mulneg1e1  8726  8th4div3  8733  halfpm6th  8734  iap0  8737  dfdec10  8979  deceq12i  8984  numltc  9001  decsuc  9006  decsucc  9016  nummac  9020  numma2c  9021  numadd  9022  numaddc  9023  nummul1c  9024  nummul2c  9025  decma  9026  decmac  9027  decma2c  9028  decadd  9029  decaddc  9030  decrmanc  9032  decrmac  9033  decaddci  9036  decsubi  9038  decmul1  9039  decmul1c  9040  decmul2c  9041  11multnc  9043  4t3lem  9072  6t2e12  9079  7t2e14  9084  8t2e16  9090  9t2e18  9097  9t11e99  9105  divfnzn  9205  xnegpnf  9394  xneg0  9397  xaddmnf1  9414  xaddmnf2  9415  mnfaddpnf  9417  iooval2  9481  dfioo2  9540  fzval2  9576  fzsuc2  9642  fztpval  9646  fzo01  9776  fzo12sn  9777  fzo0to42pr  9780  fldiv4p1lem1div2  9861  intqfrac2  9875  intfracq  9876  1tonninf  9995  dfseq3-2  10004  neg1sqe1  10180  sq2  10181  sq3  10182  cu2  10184  i2  10186  i3  10187  binom2i  10194  sq10  10252  3dec  10254  facp1  10269  fac2  10270  fac4  10272  4bc2eq6  10313  hashp1i  10349  pr0hash2ex  10354  hashfzo  10361  hashxp  10365  zfz1isolem1  10376  cji  10467  cnrecnv  10475  sqrt0  10568  resqrexlemover  10574  resqrexlemcalc3  10580  absi  10623  absimle  10648  sumeq12i  10923  summodclem2a  10939  summodc  10941  sum0  10946  fsumsplitf  10966  fsum2dlemstep  10992  fsumabs  11023  fsumiun  11035  0.999...  11079  mertenslem2  11094  ege2le3  11125  eft0val  11147  cos0  11185  cos1bnd  11214  cos2bnd  11215  3dvdsdec  11307  3dvds2dec  11308  odd2np1  11315  opoe  11337  nn0o  11349  gcd0val  11394  6gcd4e2  11426  3lcm2e6woprm  11510  3lcm2e6  11581  nn0gcdsq  11620  phiprmpw  11640  phimullem  11643  unennn  11652  strnfvnd  11678  slotslfn  11684  setsfun  11693  setsfun0  11694  setscom  11698  setsslid  11708  2strstr1g  11761  cnco  12087  cnmptid  12118  cnmetdval  12323  remetdval  12328  resubmet  12337  ex-fl  12364  ex-exp  12366  ex-fac  12367  ex-bc  12368  ex-dvds  12369  ex-gcd  12370  bj-dfom  12540  nninfsellemqall  12616