Theorem eqtri 2198

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtr2i  2199  eqtr3i  2200  eqtr4i  2201  3eqtri  2202  3eqtrri  2203  3eqtr2i  2204  cbvrab  2737  csb2  3061  cbvrabcsf  3124  difjust  3132  unjust  3134  injust  3136  dfdif3  3247  difeq12i  3253  inrot  3352  symdif1  3402  rabnc  3457  0in  3460  ssdifin0  3506  dfif3  3549  ifbieq2i  3559  ifbieq12i  3561  pwjust  3578  snjust  3599  dfpr2  3613  disjpr2  3658  difprsn1  3733  diftpsn3  3735  difpr  3736  dfuni2  3813  intab  3875  intunsn  3884  rint0  3885  iunid  3944  viin  3948  iinrabm  3951  2iunin  3955  riin0  3960  iunxprg  3969  unopab  4084  cbvmptf  4099  cbvmpt  4100  exmid1stab  4210  unisucg  4416  op1stb  4480  orddif  4548  elxpi  4644  csbxpg  4709  relopabi  4754  inxp  4763  coeq12i  4792  dfdm3  4816  dfrn3  4818  dmun  4836  dmopab  4840  dmopab3  4842  dmxpid  4850  dmxpin  4851  rnopab  4876  rnmpt  4877  rncoss  4899  rncoeq  4902  reseq12i  4907  resundi  4922  resindi  4924  resiun1  4928  resdmdfsn  4952  resopab  4953  mptresid  4963  dfima3  4975  imadisj  4992  ndmima  5007  mptcnv  5033  rnun  5039  rnuni  5042  imaundi  5043  inimass  5047  cnvxp  5049  rnxpm  5060  dminxp  5075  imainrect  5076  cnvcnv3  5080  dmpropg  5103  op1sta  5112  op2ndb  5114  op2nda  5115  resdmres  5122  mptpreima  5124  coundi  5132  coundir  5133  cocnvcnv1  5141  cores2  5143  dfdm2  5165  iotajust  5179  dfiota2  5181  funi  5250  funtp  5271  fntpg  5274  funcnvuni  5287  funcnvres  5291  imadiflem  5297  imadif  5298  imainlem  5299  imain  5300  fnresdisj  5328  mptfng  5343  resdif  5485  fv2  5512  dffv4g  5514  fveq12i  5523  nfvres  5550  0fv  5552  dfimafn2  5567  fnimapr  5578  fvmptss2  5593  fvmptg  5594  fvmpts  5596  fvmpt2  5601  mptfvex  5603  elfvmptrab  5613  fvopab6  5614  f1ompt  5669  dfmpt  5695  ressnop0  5699  fprg  5701  fvsnun1  5715  fsnunfv  5719  fvpr2g  5725  imauni  5764  fliftfuns  5801  cbvriota  5843  oveq123i  5891  fconstmpo  5972  resoprab  5973  mpofun  5979  rnmpo  5987  reldmmpo  5988  ov  5996  ovigg  5997  ovmpt4g  5999  ovg  6015  caov31  6066  elmpocl  6071  f1ocnvd  6075  oprabrexex2  6133  op1st  6149  op2nd  6150  f1stres  6162  f2ndres  6163  unielxp  6177  dfoprab3s  6193  dfoprab4  6195  mpompts  6201  mpofvex  6206  oprab2co  6221  df1st2  6222  df2nd2  6223  f1od2  6238  brtpos0  6255  tposoprab  6283  smores3  6296  tfrlemi14d  6336  tfr1onlemaccex  6351  tfrcllemaccex  6364  rdgisuc1  6387  rdg0  6390  frec0g  6400  df1o2  6432  df2o2  6434  oasuc  6467  omv2  6468  omsuc  6475  ecidsn  6584  qliftfuns  6621  oviec  6643  mapsncnv  6697  dfixp  6702  xpcomco  6828  xpassen  6832  ssenen  6853  undifdc  6925  unfiin  6927  fidcenumlemrks  6954  fidcenumlemr  6956  sbthlemi5  6962  sbthlemi8  6965  fi0  6976  inf00  7032  djuf1olemr  7055  djuinr  7064  djuin  7065  djuun  7068  casefun  7086  casedm  7087  caseinj  7090  caseinl  7092  caseinr  7093  endjusym  7097  eninl  7098  eninr  7099  djudm  7106  djuinj  7107  fodjuomni  7149  fodjumkv  7160  nninfwlporlemd  7172  pm54.43  7191  exmidfodomrlemim  7202  xp2dju  7216  djucomen  7217  djuassen  7218  xpdjuen  7219  pw1nel3  7232  sucpw1nel3  7234  addpiord  7317  mulpiord  7318  dmaddpi  7326  dmmulpi  7327  recmulnqg  7392  1lt2nq  7407  halfnqq  7411  dfmq0qs  7430  dfplq0qs  7431  genpdf  7509  1prl  7556  1pru  7557  ltexprlemell  7599  ltexprlemelu  7600  recexprlemell  7623  recexprlemelu  7624  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdrl  7658  cauappcvgprlem2  7661  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgprlem2  7681  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  caucvgprprlem2  7711  addsrpr  7746  mulsrpr  7747  caucvgsrlemoffres  7801  caucvgsr  7803  suplocsrlempr  7808  addcnsr  7835  mulcnsr  7836  mulresr  7839  addvalex  7845  pitonnlem1  7846  axi2m1  7876  axcnre  7882  mulcomli  7966  mnfnre  8002  addcomli  8104  add42i  8125  mvrraddi  8176  neg0  8205  negdii  8243  negsubdi2i  8245  crap0  8917  2t2e4  9075  3t2e6  9077  3t3e9  9078  4t2e8  9079  neg1mulneg1e1  9133  8th4div3  9140  halfpm6th  9141  iap0  9144  dfdec10  9389  deceq12i  9394  numltc  9411  decsuc  9416  decsucc  9426  nummac  9430  numma2c  9431  numadd  9432  numaddc  9433  nummul1c  9434  nummul2c  9435  decma  9436  decmac  9437  decma2c  9438  decadd  9439  decaddc  9440  decrmanc  9442  decrmac  9443  decaddci  9446  decsubi  9448  decmul1  9449  decmul1c  9450  decmul2c  9451  11multnc  9453  4t3lem  9482  6t2e12  9489  7t2e14  9494  8t2e16  9500  9t2e18  9507  9t11e99  9515  halfthird  9528  5recm6rec  9529  divfnzn  9623  xnegpnf  9830  xneg0  9833  xaddmnf1  9850  xaddmnf2  9851  mnfaddpnf  9853  iooval2  9917  dfioo2  9976  fzval2  10013  fzsuc2  10081  fztpval  10085  fz0to3un2pr  10125  fz0to4untppr  10126  fzo01  10218  fzo12sn  10219  fzo0to42pr  10222  fldiv4p1lem1div2  10307  intqfrac2  10321  intfracq  10322  1tonninf  10442  neg1sqe1  10617  sq2  10618  sq3  10619  cu2  10621  i2  10623  i3  10624  binom2i  10631  sq10  10694  3dec  10696  facp1  10712  fac2  10713  fac4  10715  4bc2eq6  10756  hashp1i  10792  pr0hash2ex  10797  hashfzo  10804  hashxp  10808  zfz1isolem1  10822  cji  10913  cnrecnv  10921  sqrt0  11015  resqrexlemover  11021  resqrexlemcalc3  11027  absi  11070  absimle  11095  sumeq12i  11375  summodclem2a  11391  summodc  11393  sum0  11398  fsumsplitf  11418  fsum2dlemstep  11444  fsumabs  11475  fsumiun  11487  0.999...  11531  mertenslem2  11546  prodeq12i  11573  prodmodc  11588  fprod2dlemstep  11632  ege2le3  11681  eft0val  11703  cos0  11740  cos1bnd  11769  cos2bnd  11770  3dvdsdec  11872  3dvds2dec  11873  odd2np1  11880  opoe  11902  nn0o  11914  gcd0val  11963  6gcd4e2  11998  nnmindc  12037  nnminle  12038  3lcm2e6woprm  12088  3lcm2e6  12162  nn0gcdsq  12202  phiprmpw  12224  phimullem  12227  pcprecl  12291  pcprendvds  12292  pcmptdvds  12345  pockthi  12358  unennn  12400  ennnfonelemj0  12404  ennnfonelem0  12408  ennnfonelem1  12410  ennnfonelemhf1o  12416  ennnfonelemrn  12422  ennnfonelemdm  12423  strnfvnd  12484  slotslfn  12490  setsfun  12499  setsfun0  12500  setscom  12504  setsslid  12515  2strstr1g  12582  eqglact  13089  rmodislmod  13446  cnco  13760  txuni2  13795  txbas  13797  uptx  13813  txcn  13814  cnmptid  13820  cnmpt2t  13832  xmetxp  14046  cnmetdval  14068  remetdval  14078  resubmet  14087  rerestcntop  14089  divcnap  14094  cnrehmeocntop  14132  dvexp  14214  sinhalfpilem  14251  cosneghalfpi  14258  efhalfpi  14259  cospi  14260  efipi  14261  eulerid  14262  sin2pi  14263  cos2pi  14264  ef2pi  14265  sincosq4sgn  14289  cosq14gt0  14292  tangtx  14298  sincos4thpi  14300  sincos6thpi  14302  sinkpi  14307  cosq34lt1  14310  dfrelog  14320  2logb9irr  14428  2logb9irrALT  14431  2logb9irrap  14434  zabsle1  14439  lgslem2  14441  lgsfcl2  14446  lgsdir2lem1  14468  lgsdir2lem2  14469  lgsdir2lem4  14471  lgsdir2lem5  14472  2lgsoddprmlem3a  14494  2lgsoddprmlem3b  14495  2lgsoddprmlem3c  14496  2lgsoddprmlem3d  14497  ex-fl  14516  ex-exp  14518  ex-fac  14519  ex-bc  14520  ex-dvds  14521  ex-gcd  14522  bj-dfom  14724  012of  14784  2o01f  14785  pwle2  14787  nninfsellemqall  14803  isomninnlem  14817  iswomninnlem  14836  ismkvnnlem  14839  dceqnconst  14846  dcapnconst  14847  taupi  14859