Theorem eqtri 2198

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtri.1	⊢ 𝐴 = 𝐵
eqtri.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eqtri	⊢ 𝐴 = 𝐶

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	eqeq2i 2188	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐴 = 𝐶)
4	1, 3	mpbi 145	1 ⊢ 𝐴 = 𝐶

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  7998  addcomli  8100  add42i  8121  mvrraddi  8172  neg0  8201  negdii  8239  negsubdi2i  8241  crap0  8913  2t2e4  9071  3t2e6  9073  3t3e9  9074  4t2e8  9075  neg1mulneg1e1  9129  8th4div3  9136  halfpm6th  9137  iap0  9140  dfdec10  9385  deceq12i  9390  numltc  9407  decsuc  9412  decsucc  9422  nummac  9426  numma2c  9427  numadd  9428  numaddc  9429  nummul1c  9430  nummul2c  9431  decma  9432  decmac  9433  decma2c  9434  decadd  9435  decaddc  9436  decrmanc  9438  decrmac  9439  decaddci  9442  decsubi  9444  decmul1  9445  decmul1c  9446  decmul2c  9447  11multnc  9449  4t3lem  9478  6t2e12  9485  7t2e14  9490  8t2e16  9496  9t2e18  9503  9t11e99  9511  halfthird  9524  5recm6rec  9525  divfnzn  9619  xnegpnf  9826  xneg0  9829  xaddmnf1  9846  xaddmnf2  9847  mnfaddpnf  9849  iooval2  9913  dfioo2  9972  fzval2  10009  fzsuc2  10076  fztpval  10080  fz0to3un2pr  10120  fz0to4untppr  10121  fzo01  10213  fzo12sn  10214  fzo0to42pr  10217  fldiv4p1lem1div2  10302  intqfrac2  10316  intfracq  10317  1tonninf  10437  neg1sqe1  10611  sq2  10612  sq3  10613  cu2  10615  i2  10617  i3  10618  binom2i  10625  sq10  10687  3dec  10689  facp1  10705  fac2  10706  fac4  10708  4bc2eq6  10749  hashp1i  10785  pr0hash2ex  10790  hashfzo  10797  hashxp  10801  zfz1isolem1  10815  cji  10906  cnrecnv  10914  sqrt0  11008  resqrexlemover  11014  resqrexlemcalc3  11020  absi  11063  absimle  11088  sumeq12i  11368  summodclem2a  11384  summodc  11386  sum0  11391  fsumsplitf  11411  fsum2dlemstep  11437  fsumabs  11468  fsumiun  11480  0.999...  11524  mertenslem2  11539  prodeq12i  11566  prodmodc  11581  fprod2dlemstep  11625  ege2le3  11674  eft0val  11696  cos0  11733  cos1bnd  11762  cos2bnd  11763  3dvdsdec  11864  3dvds2dec  11865  odd2np1  11872  opoe  11894  nn0o  11906  gcd0val  11955  6gcd4e2  11990  nnmindc  12029  nnminle  12030  3lcm2e6woprm  12080  3lcm2e6  12154  nn0gcdsq  12194  phiprmpw  12216  phimullem  12219  pcprecl  12283  pcprendvds  12284  pcmptdvds  12337  pockthi  12350  unennn  12392  ennnfonelemj0  12396  ennnfonelem0  12400  ennnfonelem1  12402  ennnfonelemhf1o  12408  ennnfonelemrn  12414  ennnfonelemdm  12415  strnfvnd  12476  slotslfn  12482  setsfun  12491  setsfun0  12492  setscom  12496  setsslid  12507  2strstr1g  12574  eqglact  13037  cnco  13614  txuni2  13649  txbas  13651  uptx  13667  txcn  13668  cnmptid  13674  cnmpt2t  13686  xmetxp  13900  cnmetdval  13922  remetdval  13932  resubmet  13941  rerestcntop  13943  divcnap  13948  cnrehmeocntop  13986  dvexp  14068  sinhalfpilem  14105  cosneghalfpi  14112  efhalfpi  14113  cospi  14114  efipi  14115  eulerid  14116  sin2pi  14117  cos2pi  14118  ef2pi  14119  sincosq4sgn  14143  cosq14gt0  14146  tangtx  14152  sincos4thpi  14154  sincos6thpi  14156  sinkpi  14161  cosq34lt1  14164  dfrelog  14174  2logb9irr  14282  2logb9irrALT  14285  2logb9irrap  14288  zabsle1  14293  lgslem2  14295  lgsfcl2  14300  lgsdir2lem1  14322  lgsdir2lem2  14323  lgsdir2lem4  14325  lgsdir2lem5  14326  ex-fl  14359  ex-exp  14361  ex-fac  14362  ex-bc  14363  ex-dvds  14364  ex-gcd  14365  bj-dfom  14567  012of  14627  2o01f  14628  pwle2  14630  nninfsellemqall  14646  isomninnlem  14660  iswomninnlem  14679  ismkvnnlem  14682  dceqnconst  14689  dcapnconst  14690  taupi  14702