Theorem eqtri 2217

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtr2i  2218  eqtr3i  2219  eqtr4i  2220  3eqtri  2221  3eqtrri  2222  3eqtr2i  2223  cbvrab  2761  csb2  3086  cbvrabcsf  3150  difjust  3158  unjust  3160  injust  3162  dfdif3  3274  difeq12i  3280  inrot  3379  symdif1  3429  rabnc  3484  0in  3487  ssdifin0  3533  dfif3  3575  ifbieq2i  3585  ifbieq12i  3587  pwjust  3607  snjust  3628  dfpr2  3642  disjpr2  3687  difprsn1  3762  diftpsn3  3764  difpr  3765  dfuni2  3842  intab  3904  intunsn  3913  rint0  3914  iunid  3973  viin  3977  iinrabm  3980  2iunin  3984  riin0  3989  iunxprg  3998  unopab  4113  cbvmptf  4128  cbvmpt  4129  exmid1stab  4242  unisucg  4450  op1stb  4514  orddif  4584  elxpi  4680  csbxpg  4745  relopabi  4792  inxp  4801  coeq12i  4830  dfdm3  4854  dfrn3  4856  dmun  4874  dmopab  4878  dmopab3  4880  dmxpid  4888  dmxpin  4889  rnopab  4914  rnmpt  4915  rncoss  4937  rncoeq  4940  reseq12i  4945  resundi  4960  resindi  4962  resiun1  4966  resdmdfsn  4990  resopab  4991  opabresid  5000  dfima3  5013  mptima  5022  imadisj  5032  ndmima  5047  mptcnv  5073  rnun  5079  rnuni  5082  imaundi  5083  inimass  5087  cnvxp  5089  rnxpm  5100  dminxp  5115  imainrect  5116  cnvcnv3  5120  dmpropg  5143  op1sta  5152  op2ndb  5154  op2nda  5155  resdmres  5162  mptpreima  5164  coundi  5172  coundir  5173  cocnvcnv1  5181  cores2  5183  dfdm2  5205  iotajust  5219  dfiota2  5221  funi  5291  funtp  5312  fntpg  5315  funcnvuni  5328  funcnvres  5332  imadiflem  5338  imadif  5339  imainlem  5340  imain  5341  fnresdisj  5371  mptfng  5386  resdif  5529  fv2  5556  dffv4g  5558  fveq12i  5567  nfvres  5595  0fv  5597  dfimafn2  5613  fnimapr  5624  fvmptss2  5639  fvmptg  5640  fvmpts  5642  fvmpt2  5648  mptfvex  5650  elfvmptrab  5660  fvopab6  5661  f1ompt  5716  dfmpt  5742  ressnop0  5746  fprg  5748  fvsnun1  5762  fsnunfv  5766  fvpr2g  5772  imauni  5811  fliftfuns  5848  cbvriota  5891  oveq123i  5939  fconstmpo  6021  resoprab  6022  mpofun  6028  rnmpo  6037  reldmmpo  6038  ov  6046  ovigg  6047  ovmpt4g  6049  ovg  6066  caov31  6117  elmpocl  6122  f1ocnvd  6129  oprabrexex2  6196  op1st  6213  op2nd  6214  f1stres  6226  f2ndres  6227  unielxp  6241  dfoprab3s  6257  dfoprab4  6259  mpompts  6265  mpofvex  6272  oprab2co  6285  df1st2  6286  df2nd2  6287  f1od2  6302  brtpos0  6319  tposoprab  6347  smores3  6360  tfrlemi14d  6400  tfr1onlemaccex  6415  tfrcllemaccex  6428  rdgisuc1  6451  rdg0  6454  frec0g  6464  df1o2  6496  df2o2  6498  oasuc  6531  omv2  6532  omsuc  6539  ecidsn  6650  qliftfuns  6687  oviec  6709  mapsncnv  6763  dfixp  6768  xpcomco  6894  xpassen  6898  ssenen  6921  undifdc  6994  unfiin  6996  fidcenumlemrks  7028  fidcenumlemr  7030  sbthlemi5  7036  sbthlemi8  7039  fi0  7050  inf00  7106  djuf1olemr  7129  djuinr  7138  djuin  7139  djuun  7142  casefun  7160  casedm  7161  caseinj  7164  caseinl  7166  caseinr  7167  endjusym  7171  eninl  7172  eninr  7173  djudm  7180  djuinj  7181  fodjuomni  7224  fodjumkv  7235  nninfwlporlemd  7247  pm54.43  7271  exmidfodomrlemim  7282  xp2dju  7300  djucomen  7301  djuassen  7302  xpdjuen  7303  pw1nel3  7316  sucpw1nel3  7318  addpiord  7402  mulpiord  7403  dmaddpi  7411  dmmulpi  7412  recmulnqg  7477  1lt2nq  7492  halfnqq  7496  dfmq0qs  7515  dfplq0qs  7516  genpdf  7594  1prl  7641  1pru  7642  ltexprlemell  7684  ltexprlemelu  7685  recexprlemell  7708  recexprlemelu  7709  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdrl  7743  cauappcvgprlem2  7746  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem2  7766  caucvgprprlemell  7771  caucvgprprlemelu  7772  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemclphr  7791  caucvgprprlemexbt  7792  caucvgprprlem2  7796  addsrpr  7831  mulsrpr  7832  caucvgsrlemoffres  7886  caucvgsr  7888  suplocsrlempr  7893  addcnsr  7920  mulcnsr  7921  mulresr  7924  addvalex  7930  pitonnlem1  7931  axi2m1  7961  axcnre  7967  mulcomli  8052  mnfnre  8088  addcomli  8190  add42i  8211  mvrraddi  8262  neg0  8291  negdii  8329  negsubdi2i  8331  crap0  9004  2t2e4  9164  3t2e6  9166  3t3e9  9167  4t2e8  9168  neg1mulneg1e1  9222  8th4div3  9229  halfpm6th  9230  iap0  9233  dfdec10  9479  deceq12i  9484  numltc  9501  decsuc  9506  decsucc  9516  nummac  9520  numma2c  9521  numadd  9522  numaddc  9523  nummul1c  9524  nummul2c  9525  decma  9526  decmac  9527  decma2c  9528  decadd  9529  decaddc  9530  decrmanc  9532  decrmac  9533  decaddci  9536  decsubi  9538  decmul1  9539  decmul1c  9540  decmul2c  9541  11multnc  9543  4t3lem  9572  6t2e12  9579  7t2e14  9584  8t2e16  9590  9t2e18  9597  9t11e99  9605  halfthird  9618  5recm6rec  9619  divfnzn  9714  xnegpnf  9922  xneg0  9925  xaddmnf1  9942  xaddmnf2  9943  mnfaddpnf  9945  iooval2  10009  dfioo2  10068  fzval2  10105  fzsuc2  10173  fztpval  10177  fz0to3un2pr  10217  fz0to4untppr  10218  fzo01  10311  fzo12sn  10312  fzo0to42pr  10315  fldiv4p1lem1div2  10414  intqfrac2  10430  intfracq  10431  xnn0nnen  10548  1tonninf  10552  neg1sqe1  10745  sq2  10746  sq3  10747  cu2  10749  i2  10751  i3  10752  binom2i  10759  sq10  10823  3dec  10825  facp1  10841  fac2  10842  fac4  10844  4bc2eq6  10885  hashp1i  10921  pr0hash2ex  10926  hashfzo  10933  hashxp  10937  zfz1isolem1  10951  elovmpowrd  10995  cji  11086  cnrecnv  11094  sqrt0  11188  resqrexlemover  11194  resqrexlemcalc3  11200  absi  11243  absimle  11268  sumeq12i  11549  summodclem2a  11565  summodc  11567  sum0  11572  fsumsplitf  11592  fsum2dlemstep  11618  fsumabs  11649  fsumiun  11661  0.999...  11705  mertenslem2  11720  prodeq12i  11747  prodmodc  11762  fprod2dlemstep  11806  ege2le3  11855  eft0val  11877  cos0  11914  cos1bnd  11943  cos2bnd  11944  3dvdsdec  12049  3dvds2dec  12050  odd2np1  12057  opoe  12079  nn0o  12091  5ndvds3  12118  5ndvds6  12119  bitsfzolem  12138  m1bits  12144  gcd0val  12154  6gcd4e2  12189  nnmindc  12228  nnminle  12229  3lcm2e6woprm  12281  3lcm2e6  12355  nn0gcdsq  12395  phiprmpw  12417  phimullem  12420  pcprecl  12485  pcprendvds  12486  pcmptdvds  12541  pockthi  12554  4sqlem13m  12599  4sqlem14  12600  4sqlem17  12603  4sqlem18  12604  4sqlem19  12605  dec5nprm  12610  dec2nprm  12611  modxai  12612  modsubi  12615  numexp2x  12621  decsplit0b  12622  decsplit0  12623  decsplit  12625  karatsuba  12626  2exp5  12628  2exp7  12630  2exp8  12631  2exp11  12632  2exp16  12633  3exp3  12634  unennn  12641  ennnfonelemj0  12645  ennnfonelem0  12649  ennnfonelem1  12651  ennnfonelemhf1o  12657  ennnfonelemrn  12663  ennnfonelemdm  12664  strnfvnd  12725  slotslfn  12731  setsfun  12740  setsfun0  12741  setscom  12745  setsslid  12756  2strstr1g  12826  eqglact  13433  ecqusaddd  13446  ghmeqker  13479  dfrhm2  13788  rmodislmod  13985  cnfldadd  14196  cnfldmul  14198  expghmap  14241  fczpsrbag  14305  cnco  14565  txuni2  14600  txbas  14602  uptx  14618  txcn  14619  cnmptid  14625  cnmpt2t  14637  xmetxp  14851  cnmetdval  14873  remetdval  14891  resubmet  14900  rerestcntop  14902  rerest  14904  divcnap  14909  cnrehmeocntop  14954  dvexp  15055  plyun0  15080  plyco  15103  plycj  15105  sinhalfpilem  15135  cosneghalfpi  15142  efhalfpi  15143  cospi  15144  efipi  15145  eulerid  15146  sin2pi  15147  cos2pi  15148  ef2pi  15149  sincosq4sgn  15173  cosq14gt0  15176  tangtx  15182  sincos4thpi  15184  sincos6thpi  15186  sinkpi  15191  cosq34lt1  15194  dfrelog  15204  2logb9irr  15315  2logb9irrALT  15318  2logb9irrap  15321  mersenne  15341  perfectlem2  15344  zabsle1  15348  lgslem2  15350  lgsfcl2  15355  lgsdir2lem1  15377  lgsdir2lem2  15378  lgsdir2lem4  15380  lgsdir2lem5  15381  lgseisen  15423  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgs2  15451  2lgsoddprmlem3a  15456  2lgsoddprmlem3b  15457  2lgsoddprmlem3c  15458  2lgsoddprmlem3d  15459  ex-fl  15479  ex-exp  15481  ex-fac  15482  ex-bc  15483  ex-dvds  15484  ex-gcd  15485  bj-dfom  15687  012of  15748  2o01f  15749  pwle2  15753  nninfsellemqall  15770  isomninnlem  15787  iswomninnlem  15806  ismkvnnlem  15809  dceqnconst  15817  dcapnconst  15818  taupi  15830