Theorem eqtri 2191

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 2181	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐴 = 𝐶)
4	1, 3	mpbi 144	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  eqtr2i  2192  eqtr3i  2193  eqtr4i  2194  3eqtri  2195  3eqtrri  2196  3eqtr2i  2197  cbvrab  2728  csb2  3051  cbvrabcsf  3114  difjust  3122  unjust  3124  injust  3126  dfdif3  3237  difeq12i  3243  inrot  3342  symdif1  3392  rabnc  3447  0in  3450  ssdifin0  3496  dfif3  3539  ifbieq2i  3549  ifbieq12i  3551  pwjust  3567  snjust  3588  dfpr2  3602  disjpr2  3647  difprsn1  3719  diftpsn3  3721  difpr  3722  dfuni2  3798  intab  3860  intunsn  3869  rint0  3870  iunid  3928  viin  3932  iinrabm  3935  2iunin  3939  riin0  3944  iunxprg  3953  unopab  4068  cbvmptf  4083  cbvmpt  4084  unisucg  4399  op1stb  4463  orddif  4531  elxpi  4627  csbxpg  4692  relopabi  4737  inxp  4745  coeq12i  4774  dfdm3  4798  dfrn3  4800  dmun  4818  dmopab  4822  dmopab3  4824  dmxpid  4832  dmxpin  4833  rnopab  4858  rnmpt  4859  rncoss  4881  rncoeq  4884  reseq12i  4889  resundi  4904  resindi  4906  resiun1  4910  resdmdfsn  4934  resopab  4935  mptresid  4945  dfima3  4956  imadisj  4973  ndmima  4988  mptcnv  5013  rnun  5019  rnuni  5022  imaundi  5023  inimass  5027  cnvxp  5029  rnxpm  5040  dminxp  5055  imainrect  5056  cnvcnv3  5060  dmpropg  5083  op1sta  5092  op2ndb  5094  op2nda  5095  resdmres  5102  mptpreima  5104  coundi  5112  coundir  5113  cocnvcnv1  5121  cores2  5123  dfdm2  5145  iotajust  5159  dfiota2  5161  funi  5230  funtp  5251  fntpg  5254  funcnvuni  5267  funcnvres  5271  imadiflem  5277  imadif  5278  imainlem  5279  imain  5280  fnresdisj  5308  mptfng  5323  resdif  5464  fv2  5491  dffv4g  5493  fveq12i  5502  nfvres  5529  0fv  5531  dfimafn2  5546  fnimapr  5556  fvmptss2  5571  fvmptg  5572  fvmpts  5574  fvmpt2  5579  mptfvex  5581  elfvmptrab  5591  fvopab6  5592  f1ompt  5647  dfmpt  5673  ressnop0  5677  fprg  5679  fvsnun1  5693  fsnunfv  5697  fvpr2g  5703  imauni  5740  fliftfuns  5777  cbvriota  5819  oveq123i  5867  fconstmpo  5948  resoprab  5949  mpofun  5955  rnmpo  5963  reldmmpo  5964  ov  5972  ovigg  5973  ovmpt4g  5975  ovg  5991  caov31  6042  elmpocl  6047  f1ocnvd  6051  oprabrexex2  6109  op1st  6125  op2nd  6126  f1stres  6138  f2ndres  6139  unielxp  6153  dfoprab3s  6169  dfoprab4  6171  mpompts  6177  mpofvex  6182  oprab2co  6197  df1st2  6198  df2nd2  6199  f1od2  6214  brtpos0  6231  tposoprab  6259  smores3  6272  tfrlemi14d  6312  tfr1onlemaccex  6327  tfrcllemaccex  6340  rdgisuc1  6363  rdg0  6366  frec0g  6376  df1o2  6408  df2o2  6410  oasuc  6443  omv2  6444  omsuc  6451  ecidsn  6560  qliftfuns  6597  oviec  6619  mapsncnv  6673  dfixp  6678  xpcomco  6804  xpassen  6808  ssenen  6829  undifdc  6901  unfiin  6903  fidcenumlemrks  6930  fidcenumlemr  6932  sbthlemi5  6938  sbthlemi8  6941  fi0  6952  inf00  7008  djuf1olemr  7031  djuinr  7040  djuin  7041  djuun  7044  casefun  7062  casedm  7063  caseinj  7066  caseinl  7068  caseinr  7069  endjusym  7073  eninl  7074  eninr  7075  djudm  7082  djuinj  7083  fodjuomni  7125  fodjumkv  7136  nninfwlporlemd  7148  pm54.43  7167  exmidfodomrlemim  7178  xp2dju  7192  djucomen  7193  djuassen  7194  xpdjuen  7195  pw1nel3  7208  sucpw1nel3  7210  addpiord  7278  mulpiord  7279  dmaddpi  7287  dmmulpi  7288  recmulnqg  7353  1lt2nq  7368  halfnqq  7372  dfmq0qs  7391  dfplq0qs  7392  genpdf  7470  1prl  7517  1pru  7518  ltexprlemell  7560  ltexprlemelu  7561  recexprlemell  7584  recexprlemelu  7585  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdrl  7619  cauappcvgprlem2  7622  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem2  7642  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlem2  7672  addsrpr  7707  mulsrpr  7708  caucvgsrlemoffres  7762  caucvgsr  7764  suplocsrlempr  7769  addcnsr  7796  mulcnsr  7797  mulresr  7800  addvalex  7806  pitonnlem1  7807  axi2m1  7837  axcnre  7843  mulcomli  7927  mnfnre  7962  addcomli  8064  add42i  8085  mvrraddi  8136  neg0  8165  negdii  8203  negsubdi2i  8205  crap0  8874  2t2e4  9032  3t2e6  9034  3t3e9  9035  4t2e8  9036  neg1mulneg1e1  9090  8th4div3  9097  halfpm6th  9098  iap0  9101  dfdec10  9346  deceq12i  9351  numltc  9368  decsuc  9373  decsucc  9383  nummac  9387  numma2c  9388  numadd  9389  numaddc  9390  nummul1c  9391  nummul2c  9392  decma  9393  decmac  9394  decma2c  9395  decadd  9396  decaddc  9397  decrmanc  9399  decrmac  9400  decaddci  9403  decsubi  9405  decmul1  9406  decmul1c  9407  decmul2c  9408  11multnc  9410  4t3lem  9439  6t2e12  9446  7t2e14  9451  8t2e16  9457  9t2e18  9464  9t11e99  9472  halfthird  9485  5recm6rec  9486  divfnzn  9580  xnegpnf  9785  xneg0  9788  xaddmnf1  9805  xaddmnf2  9806  mnfaddpnf  9808  iooval2  9872  dfioo2  9931  fzval2  9968  fzsuc2  10035  fztpval  10039  fz0to3un2pr  10079  fz0to4untppr  10080  fzo01  10172  fzo12sn  10173  fzo0to42pr  10176  fldiv4p1lem1div2  10261  intqfrac2  10275  intfracq  10276  1tonninf  10396  neg1sqe1  10570  sq2  10571  sq3  10572  cu2  10574  i2  10576  i3  10577  binom2i  10584  sq10  10646  3dec  10648  facp1  10664  fac2  10665  fac4  10667  4bc2eq6  10708  hashp1i  10745  pr0hash2ex  10750  hashfzo  10757  hashxp  10761  zfz1isolem1  10775  cji  10866  cnrecnv  10874  sqrt0  10968  resqrexlemover  10974  resqrexlemcalc3  10980  absi  11023  absimle  11048  sumeq12i  11328  summodclem2a  11344  summodc  11346  sum0  11351  fsumsplitf  11371  fsum2dlemstep  11397  fsumabs  11428  fsumiun  11440  0.999...  11484  mertenslem2  11499  prodeq12i  11526  prodmodc  11541  fprod2dlemstep  11585  ege2le3  11634  eft0val  11656  cos0  11693  cos1bnd  11722  cos2bnd  11723  3dvdsdec  11824  3dvds2dec  11825  odd2np1  11832  opoe  11854  nn0o  11866  gcd0val  11915  6gcd4e2  11950  nnmindc  11989  nnminle  11990  3lcm2e6woprm  12040  3lcm2e6  12114  nn0gcdsq  12154  phiprmpw  12176  phimullem  12179  pcprecl  12243  pcprendvds  12244  pcmptdvds  12297  pockthi  12310  unennn  12352  ennnfonelemj0  12356  ennnfonelem0  12360  ennnfonelem1  12362  ennnfonelemhf1o  12368  ennnfonelemrn  12374  ennnfonelemdm  12375  strnfvnd  12436  slotslfn  12442  setsfun  12451  setsfun0  12452  setscom  12456  setsslid  12466  2strstr1g  12521  cnco  13015  txuni2  13050  txbas  13052  uptx  13068  txcn  13069  cnmptid  13075  cnmpt2t  13087  xmetxp  13301  cnmetdval  13323  remetdval  13333  resubmet  13342  rerestcntop  13344  divcnap  13349  cnrehmeocntop  13387  dvexp  13469  sinhalfpilem  13506  cosneghalfpi  13513  efhalfpi  13514  cospi  13515  efipi  13516  eulerid  13517  sin2pi  13518  cos2pi  13519  ef2pi  13520  sincosq4sgn  13544  cosq14gt0  13547  tangtx  13553  sincos4thpi  13555  sincos6thpi  13557  sinkpi  13562  cosq34lt1  13565  dfrelog  13575  2logb9irr  13683  2logb9irrALT  13686  2logb9irrap  13689  zabsle1  13694  lgslem2  13696  lgsfcl2  13701  lgsdir2lem1  13723  lgsdir2lem2  13724  lgsdir2lem4  13726  lgsdir2lem5  13727  ex-fl  13760  ex-exp  13762  ex-fac  13763  ex-bc  13764  ex-dvds  13765  ex-gcd  13766  bj-dfom  13968  012of  14028  2o01f  14029  pwle2  14031  exmid1stab  14033  nninfsellemqall  14048  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084  dceqnconst  14091  dcapnconst  14092  taupi  14102