Theorem eqtri 2178

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

Syntax hints:   = wceq 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  eqtr2i  2179  eqtr3i  2180  eqtr4i  2181  3eqtri  2182  3eqtrri  2183  3eqtr2i  2184  cbvrab  2710  csb2  3033  cbvrabcsf  3096  difjust  3103  unjust  3105  injust  3107  dfdif3  3217  difeq12i  3223  inrot  3322  symdif1  3372  rabnc  3426  0in  3429  ssdifin0  3475  dfif3  3518  ifbieq2i  3528  ifbieq12i  3530  pwjust  3544  snjust  3565  dfpr2  3579  disjpr2  3623  difprsn1  3695  diftpsn3  3697  difpr  3698  dfuni2  3774  intab  3836  intunsn  3845  rint0  3846  iunid  3904  viin  3908  iinrabm  3911  2iunin  3915  riin0  3920  iunxprg  3929  unopab  4043  cbvmptf  4058  cbvmpt  4059  unisucg  4373  op1stb  4436  orddif  4504  elxpi  4599  csbxpg  4664  relopabi  4709  inxp  4717  coeq12i  4746  dfdm3  4770  dfrn3  4772  dmun  4790  dmopab  4794  dmopab3  4796  dmxpid  4804  dmxpin  4805  rnopab  4830  rnmpt  4831  rncoss  4853  rncoeq  4856  reseq12i  4861  resundi  4876  resindi  4878  resiun1  4882  resdmdfsn  4906  resopab  4907  mptresid  4917  dfima3  4928  imadisj  4945  ndmima  4960  mptcnv  4985  rnun  4991  rnuni  4994  imaundi  4995  inimass  4999  cnvxp  5001  rnxpm  5012  dminxp  5027  imainrect  5028  cnvcnv3  5032  dmpropg  5055  op1sta  5064  op2ndb  5066  op2nda  5067  resdmres  5074  mptpreima  5076  coundi  5084  coundir  5085  cocnvcnv1  5093  cores2  5095  dfdm2  5117  iotajust  5131  dfiota2  5133  funi  5199  funtp  5220  fntpg  5223  funcnvuni  5236  funcnvres  5240  imadiflem  5246  imadif  5247  imainlem  5248  imain  5249  fnresdisj  5277  mptfng  5292  resdif  5433  fv2  5460  dffv4g  5462  fveq12i  5471  nfvres  5498  0fv  5500  dfimafn2  5515  fnimapr  5525  fvmptss2  5540  fvmptg  5541  fvmpts  5543  fvmpt2  5548  mptfvex  5550  elfvmptrab  5560  fvopab6  5561  f1ompt  5615  dfmpt  5641  ressnop0  5645  fprg  5647  fvsnun1  5661  fsnunfv  5665  fvpr2g  5671  imauni  5706  fliftfuns  5743  cbvriota  5784  oveq123i  5832  fconstmpo  5910  resoprab  5911  mpofun  5917  rnmpo  5925  reldmmpo  5926  ov  5934  ovigg  5935  ovmpt4g  5937  ovg  5953  caov31  6004  elmpocl  6012  f1ocnvd  6016  oprabrexex2  6072  op1st  6088  op2nd  6089  f1stres  6101  f2ndres  6102  unielxp  6116  dfoprab3s  6132  dfoprab4  6134  mpompts  6140  mpofvex  6145  oprab2co  6159  df1st2  6160  df2nd2  6161  f1od2  6176  brtpos0  6193  tposoprab  6221  smores3  6234  tfrlemi14d  6274  tfr1onlemaccex  6289  tfrcllemaccex  6302  rdgisuc1  6325  rdg0  6328  frec0g  6338  df1o2  6370  df2o2  6372  oasuc  6404  omv2  6405  omsuc  6412  ecidsn  6520  qliftfuns  6557  oviec  6579  mapsncnv  6633  dfixp  6638  xpcomco  6764  xpassen  6768  ssenen  6789  undifdc  6861  unfiin  6863  fidcenumlemrks  6890  fidcenumlemr  6892  sbthlemi5  6898  sbthlemi8  6901  fi0  6912  inf00  6967  djuf1olemr  6988  djuinr  6997  djuin  6998  djuun  7001  casefun  7019  casedm  7020  caseinj  7023  caseinl  7025  caseinr  7026  endjusym  7030  eninl  7031  eninr  7032  djudm  7039  djuinj  7040  fodjuomni  7075  fodjumkv  7086  pm54.43  7108  exmidfodomrlemim  7119  xp2dju  7133  djucomen  7134  djuassen  7135  xpdjuen  7136  pw1nel3  7149  sucpw1nel3  7151  addpiord  7219  mulpiord  7220  dmaddpi  7228  dmmulpi  7229  recmulnqg  7294  1lt2nq  7309  halfnqq  7313  dfmq0qs  7332  dfplq0qs  7333  genpdf  7411  1prl  7458  1pru  7459  ltexprlemell  7501  ltexprlemelu  7502  recexprlemell  7525  recexprlemelu  7526  cauappcvgprlemm  7548  cauappcvgprlemopl  7549  cauappcvgprlemlol  7550  cauappcvgprlemopu  7551  cauappcvgprlemupu  7552  cauappcvgprlemdisj  7554  cauappcvgprlemloc  7555  cauappcvgprlemladdfu  7557  cauappcvgprlemladdfl  7558  cauappcvgprlemladdrl  7560  cauappcvgprlem2  7563  caucvgprlemm  7571  caucvgprlemopl  7572  caucvgprlemlol  7573  caucvgprlemopu  7574  caucvgprlemupu  7575  caucvgprlemdisj  7577  caucvgprlemloc  7578  caucvgprlemcl  7579  caucvgprlemladdfu  7580  caucvgprlemladdrl  7581  caucvgprlem2  7583  caucvgprprlemell  7588  caucvgprprlemelu  7589  caucvgprprlemml  7597  caucvgprprlemmu  7598  caucvgprprlemclphr  7608  caucvgprprlemexbt  7609  caucvgprprlem2  7613  addsrpr  7648  mulsrpr  7649  caucvgsrlemoffres  7703  caucvgsr  7705  suplocsrlempr  7710  addcnsr  7737  mulcnsr  7738  mulresr  7741  addvalex  7747  pitonnlem1  7748  axi2m1  7778  axcnre  7784  mulcomli  7868  mnfnre  7903  addcomli  8003  add42i  8024  mvrraddi  8075  neg0  8104  negdii  8142  negsubdi2i  8144  crap0  8812  2t2e4  8970  3t2e6  8972  3t3e9  8973  4t2e8  8974  neg1mulneg1e1  9028  8th4div3  9035  halfpm6th  9036  iap0  9039  dfdec10  9281  deceq12i  9286  numltc  9303  decsuc  9308  decsucc  9318  nummac  9322  numma2c  9323  numadd  9324  numaddc  9325  nummul1c  9326  nummul2c  9327  decma  9328  decmac  9329  decma2c  9330  decadd  9331  decaddc  9332  decrmanc  9334  decrmac  9335  decaddci  9338  decsubi  9340  decmul1  9341  decmul1c  9342  decmul2c  9343  11multnc  9345  4t3lem  9374  6t2e12  9381  7t2e14  9386  8t2e16  9392  9t2e18  9399  9t11e99  9407  halfthird  9420  5recm6rec  9421  divfnzn  9512  xnegpnf  9714  xneg0  9717  xaddmnf1  9734  xaddmnf2  9735  mnfaddpnf  9737  iooval2  9801  dfioo2  9860  fzval2  9897  fzsuc2  9963  fztpval  9967  fzo01  10097  fzo12sn  10098  fzo0to42pr  10101  fldiv4p1lem1div2  10186  intqfrac2  10200  intfracq  10201  1tonninf  10321  neg1sqe1  10495  sq2  10496  sq3  10497  cu2  10499  i2  10501  i3  10502  binom2i  10509  sq10  10568  3dec  10570  facp1  10586  fac2  10587  fac4  10589  4bc2eq6  10630  hashp1i  10666  pr0hash2ex  10671  hashfzo  10678  hashxp  10682  zfz1isolem1  10693  cji  10784  cnrecnv  10792  sqrt0  10886  resqrexlemover  10892  resqrexlemcalc3  10898  absi  10941  absimle  10966  sumeq12i  11244  summodclem2a  11260  summodc  11262  sum0  11267  fsumsplitf  11287  fsum2dlemstep  11313  fsumabs  11344  fsumiun  11356  0.999...  11400  mertenslem2  11415  prodeq12i  11442  prodmodc  11457  fprod2dlemstep  11501  ege2le3  11550  eft0val  11572  cos0  11609  cos1bnd  11638  cos2bnd  11639  3dvdsdec  11737  3dvds2dec  11738  odd2np1  11745  opoe  11767  nn0o  11779  gcd0val  11824  6gcd4e2  11859  3lcm2e6woprm  11943  3lcm2e6  12014  nn0gcdsq  12054  phiprmpw  12074  phimullem  12077  unennn  12098  ennnfonelemj0  12102  ennnfonelem0  12106  ennnfonelem1  12108  ennnfonelemhf1o  12114  ennnfonelemrn  12120  ennnfonelemdm  12121  strnfvnd  12170  slotslfn  12176  setsfun  12185  setsfun0  12186  setscom  12190  setsslid  12200  2strstr1g  12253  cnco  12581  txuni2  12616  txbas  12618  uptx  12634  txcn  12635  cnmptid  12641  cnmpt2t  12653  xmetxp  12867  cnmetdval  12889  remetdval  12899  resubmet  12908  rerestcntop  12910  divcnap  12915  cnrehmeocntop  12953  dvexp  13035  sinhalfpilem  13072  cosneghalfpi  13079  efhalfpi  13080  cospi  13081  efipi  13082  eulerid  13083  sin2pi  13084  cos2pi  13085  ef2pi  13086  sincosq4sgn  13110  cosq14gt0  13113  tangtx  13119  sincos4thpi  13121  sincos6thpi  13123  sinkpi  13128  cosq34lt1  13131  dfrelog  13141  2logb9irr  13248  2logb9irrALT  13251  2logb9irrap  13254  ex-fl  13260  ex-exp  13262  ex-fac  13263  ex-bc  13264  ex-dvds  13265  ex-gcd  13266  bj-dfom  13467  012of  13527  2o01f  13528  pwle2  13530  exmid1stab  13532  nninfsellemqall  13549  isomninnlem  13563  iswomninnlem  13582  ismkvnnlem  13585  dceqnconst  13592  dcapnconst  13593  taupi  13603