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  2735  csb2  3059  cbvrabcsf  3122  difjust  3130  unjust  3132  injust  3134  dfdif3  3245  difeq12i  3251  inrot  3350  symdif1  3400  rabnc  3455  0in  3458  ssdifin0  3504  dfif3  3547  ifbieq2i  3557  ifbieq12i  3559  pwjust  3576  snjust  3597  dfpr2  3611  disjpr2  3656  difprsn1  3731  diftpsn3  3733  difpr  3734  dfuni2  3811  intab  3873  intunsn  3882  rint0  3883  iunid  3942  viin  3946  iinrabm  3949  2iunin  3953  riin0  3958  iunxprg  3967  unopab  4082  cbvmptf  4097  cbvmpt  4098  exmid1stab  4208  unisucg  4414  op1stb  4478  orddif  4546  elxpi  4642  csbxpg  4707  relopabi  4752  inxp  4761  coeq12i  4790  dfdm3  4814  dfrn3  4816  dmun  4834  dmopab  4838  dmopab3  4840  dmxpid  4848  dmxpin  4849  rnopab  4874  rnmpt  4875  rncoss  4897  rncoeq  4900  reseq12i  4905  resundi  4920  resindi  4922  resiun1  4926  resdmdfsn  4950  resopab  4951  mptresid  4961  dfima3  4973  imadisj  4990  ndmima  5005  mptcnv  5031  rnun  5037  rnuni  5040  imaundi  5041  inimass  5045  cnvxp  5047  rnxpm  5058  dminxp  5073  imainrect  5074  cnvcnv3  5078  dmpropg  5101  op1sta  5110  op2ndb  5112  op2nda  5113  resdmres  5120  mptpreima  5122  coundi  5130  coundir  5131  cocnvcnv1  5139  cores2  5141  dfdm2  5163  iotajust  5177  dfiota2  5179  funi  5248  funtp  5269  fntpg  5272  funcnvuni  5285  funcnvres  5289  imadiflem  5295  imadif  5296  imainlem  5297  imain  5298  fnresdisj  5326  mptfng  5341  resdif  5483  fv2  5510  dffv4g  5512  fveq12i  5521  nfvres  5548  0fv  5550  dfimafn2  5565  fnimapr  5576  fvmptss2  5591  fvmptg  5592  fvmpts  5594  fvmpt2  5599  mptfvex  5601  elfvmptrab  5611  fvopab6  5612  f1ompt  5667  dfmpt  5693  ressnop0  5697  fprg  5699  fvsnun1  5713  fsnunfv  5717  fvpr2g  5723  imauni  5761  fliftfuns  5798  cbvriota  5840  oveq123i  5888  fconstmpo  5969  resoprab  5970  mpofun  5976  rnmpo  5984  reldmmpo  5985  ov  5993  ovigg  5994  ovmpt4g  5996  ovg  6012  caov31  6063  elmpocl  6068  f1ocnvd  6072  oprabrexex2  6130  op1st  6146  op2nd  6147  f1stres  6159  f2ndres  6160  unielxp  6174  dfoprab3s  6190  dfoprab4  6192  mpompts  6198  mpofvex  6203  oprab2co  6218  df1st2  6219  df2nd2  6220  f1od2  6235  brtpos0  6252  tposoprab  6280  smores3  6293  tfrlemi14d  6333  tfr1onlemaccex  6348  tfrcllemaccex  6361  rdgisuc1  6384  rdg0  6387  frec0g  6397  df1o2  6429  df2o2  6431  oasuc  6464  omv2  6465  omsuc  6472  ecidsn  6581  qliftfuns  6618  oviec  6640  mapsncnv  6694  dfixp  6699  xpcomco  6825  xpassen  6829  ssenen  6850  undifdc  6922  unfiin  6924  fidcenumlemrks  6951  fidcenumlemr  6953  sbthlemi5  6959  sbthlemi8  6962  fi0  6973  inf00  7029  djuf1olemr  7052  djuinr  7061  djuin  7062  djuun  7065  casefun  7083  casedm  7084  caseinj  7087  caseinl  7089  caseinr  7090  endjusym  7094  eninl  7095  eninr  7096  djudm  7103  djuinj  7104  fodjuomni  7146  fodjumkv  7157  nninfwlporlemd  7169  pm54.43  7188  exmidfodomrlemim  7199  xp2dju  7213  djucomen  7214  djuassen  7215  xpdjuen  7216  pw1nel3  7229  sucpw1nel3  7231  addpiord  7314  mulpiord  7315  dmaddpi  7323  dmmulpi  7324  recmulnqg  7389  1lt2nq  7404  halfnqq  7408  dfmq0qs  7427  dfplq0qs  7428  genpdf  7506  1prl  7553  1pru  7554  ltexprlemell  7596  ltexprlemelu  7597  recexprlemell  7620  recexprlemelu  7621  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdrl  7655  cauappcvgprlem2  7658  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem2  7678  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem2  7708  addsrpr  7743  mulsrpr  7744  caucvgsrlemoffres  7798  caucvgsr  7800  suplocsrlempr  7805  addcnsr  7832  mulcnsr  7833  mulresr  7836  addvalex  7842  pitonnlem1  7843  axi2m1  7873  axcnre  7879  mulcomli  7963  mnfnre  7999  addcomli  8101  add42i  8122  mvrraddi  8173  neg0  8202  negdii  8240  negsubdi2i  8242  crap0  8914  2t2e4  9072  3t2e6  9074  3t3e9  9075  4t2e8  9076  neg1mulneg1e1  9130  8th4div3  9137  halfpm6th  9138  iap0  9141  dfdec10  9386  deceq12i  9391  numltc  9408  decsuc  9413  decsucc  9423  nummac  9427  numma2c  9428  numadd  9429  numaddc  9430  nummul1c  9431  nummul2c  9432  decma  9433  decmac  9434  decma2c  9435  decadd  9436  decaddc  9437  decrmanc  9439  decrmac  9440  decaddci  9443  decsubi  9445  decmul1  9446  decmul1c  9447  decmul2c  9448  11multnc  9450  4t3lem  9479  6t2e12  9486  7t2e14  9491  8t2e16  9497  9t2e18  9504  9t11e99  9512  halfthird  9525  5recm6rec  9526  divfnzn  9620  xnegpnf  9827  xneg0  9830  xaddmnf1  9847  xaddmnf2  9848  mnfaddpnf  9850  iooval2  9914  dfioo2  9973  fzval2  10010  fzsuc2  10078  fztpval  10082  fz0to3un2pr  10122  fz0to4untppr  10123  fzo01  10215  fzo12sn  10216  fzo0to42pr  10219  fldiv4p1lem1div2  10304  intqfrac2  10318  intfracq  10319  1tonninf  10439  neg1sqe1  10614  sq2  10615  sq3  10616  cu2  10618  i2  10620  i3  10621  binom2i  10628  sq10  10691  3dec  10693  facp1  10709  fac2  10710  fac4  10712  4bc2eq6  10753  hashp1i  10789  pr0hash2ex  10794  hashfzo  10801  hashxp  10805  zfz1isolem1  10819  cji  10910  cnrecnv  10918  sqrt0  11012  resqrexlemover  11018  resqrexlemcalc3  11024  absi  11067  absimle  11092  sumeq12i  11372  summodclem2a  11388  summodc  11390  sum0  11395  fsumsplitf  11415  fsum2dlemstep  11441  fsumabs  11472  fsumiun  11484  0.999...  11528  mertenslem2  11543  prodeq12i  11570  prodmodc  11585  fprod2dlemstep  11629  ege2le3  11678  eft0val  11700  cos0  11737  cos1bnd  11766  cos2bnd  11767  3dvdsdec  11869  3dvds2dec  11870  odd2np1  11877  opoe  11899  nn0o  11911  gcd0val  11960  6gcd4e2  11995  nnmindc  12034  nnminle  12035  3lcm2e6woprm  12085  3lcm2e6  12159  nn0gcdsq  12199  phiprmpw  12221  phimullem  12224  pcprecl  12288  pcprendvds  12289  pcmptdvds  12342  pockthi  12355  unennn  12397  ennnfonelemj0  12401  ennnfonelem0  12405  ennnfonelem1  12407  ennnfonelemhf1o  12413  ennnfonelemrn  12419  ennnfonelemdm  12420  strnfvnd  12481  slotslfn  12487  setsfun  12496  setsfun0  12497  setscom  12501  setsslid  12512  2strstr1g  12579  eqglact  13082  cnco  13691  txuni2  13726  txbas  13728  uptx  13744  txcn  13745  cnmptid  13751  cnmpt2t  13763  xmetxp  13977  cnmetdval  13999  remetdval  14009  resubmet  14018  rerestcntop  14020  divcnap  14025  cnrehmeocntop  14063  dvexp  14145  sinhalfpilem  14182  cosneghalfpi  14189  efhalfpi  14190  cospi  14191  efipi  14192  eulerid  14193  sin2pi  14194  cos2pi  14195  ef2pi  14196  sincosq4sgn  14220  cosq14gt0  14223  tangtx  14229  sincos4thpi  14231  sincos6thpi  14233  sinkpi  14238  cosq34lt1  14241  dfrelog  14251  2logb9irr  14359  2logb9irrALT  14362  2logb9irrap  14365  zabsle1  14370  lgslem2  14372  lgsfcl2  14377  lgsdir2lem1  14399  lgsdir2lem2  14400  lgsdir2lem4  14402  lgsdir2lem5  14403  2lgsoddprmlem3a  14425  2lgsoddprmlem3b  14426  2lgsoddprmlem3c  14427  2lgsoddprmlem3d  14428  ex-fl  14447  ex-exp  14449  ex-fac  14450  ex-bc  14451  ex-dvds  14452  ex-gcd  14453  bj-dfom  14655  012of  14715  2o01f  14716  pwle2  14718  nninfsellemqall  14734  isomninnlem  14748  iswomninnlem  14767  ismkvnnlem  14770  dceqnconst  14777  dcapnconst  14778  taupi  14790