Theorem eqtri 2214

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 2204	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtr2i  2215  eqtr3i  2216  eqtr4i  2217  3eqtri  2218  3eqtrri  2219  3eqtr2i  2220  cbvrab  2758  csb2  3082  cbvrabcsf  3146  difjust  3154  unjust  3156  injust  3158  dfdif3  3269  difeq12i  3275  inrot  3374  symdif1  3424  rabnc  3479  0in  3482  ssdifin0  3528  dfif3  3570  ifbieq2i  3580  ifbieq12i  3582  pwjust  3602  snjust  3623  dfpr2  3637  disjpr2  3682  difprsn1  3757  diftpsn3  3759  difpr  3760  dfuni2  3837  intab  3899  intunsn  3908  rint0  3909  iunid  3968  viin  3972  iinrabm  3975  2iunin  3979  riin0  3984  iunxprg  3993  unopab  4108  cbvmptf  4123  cbvmpt  4124  exmid1stab  4237  unisucg  4445  op1stb  4509  orddif  4579  elxpi  4675  csbxpg  4740  relopabi  4787  inxp  4796  coeq12i  4825  dfdm3  4849  dfrn3  4851  dmun  4869  dmopab  4873  dmopab3  4875  dmxpid  4883  dmxpin  4884  rnopab  4909  rnmpt  4910  rncoss  4932  rncoeq  4935  reseq12i  4940  resundi  4955  resindi  4957  resiun1  4961  resdmdfsn  4985  resopab  4986  opabresid  4995  dfima3  5008  mptima  5017  imadisj  5027  ndmima  5042  mptcnv  5068  rnun  5074  rnuni  5077  imaundi  5078  inimass  5082  cnvxp  5084  rnxpm  5095  dminxp  5110  imainrect  5111  cnvcnv3  5115  dmpropg  5138  op1sta  5147  op2ndb  5149  op2nda  5150  resdmres  5157  mptpreima  5159  coundi  5167  coundir  5168  cocnvcnv1  5176  cores2  5178  dfdm2  5200  iotajust  5214  dfiota2  5216  funi  5286  funtp  5307  fntpg  5310  funcnvuni  5323  funcnvres  5327  imadiflem  5333  imadif  5334  imainlem  5335  imain  5336  fnresdisj  5364  mptfng  5379  resdif  5522  fv2  5549  dffv4g  5551  fveq12i  5560  nfvres  5588  0fv  5590  dfimafn2  5606  fnimapr  5617  fvmptss2  5632  fvmptg  5633  fvmpts  5635  fvmpt2  5641  mptfvex  5643  elfvmptrab  5653  fvopab6  5654  f1ompt  5709  dfmpt  5735  ressnop0  5739  fprg  5741  fvsnun1  5755  fsnunfv  5759  fvpr2g  5765  imauni  5804  fliftfuns  5841  cbvriota  5884  oveq123i  5932  fconstmpo  6013  resoprab  6014  mpofun  6020  rnmpo  6029  reldmmpo  6030  ov  6038  ovigg  6039  ovmpt4g  6041  ovg  6057  caov31  6108  elmpocl  6113  f1ocnvd  6120  oprabrexex2  6182  op1st  6199  op2nd  6200  f1stres  6212  f2ndres  6213  unielxp  6227  dfoprab3s  6243  dfoprab4  6245  mpompts  6251  mpofvex  6256  oprab2co  6271  df1st2  6272  df2nd2  6273  f1od2  6288  brtpos0  6305  tposoprab  6333  smores3  6346  tfrlemi14d  6386  tfr1onlemaccex  6401  tfrcllemaccex  6414  rdgisuc1  6437  rdg0  6440  frec0g  6450  df1o2  6482  df2o2  6484  oasuc  6517  omv2  6518  omsuc  6525  ecidsn  6636  qliftfuns  6673  oviec  6695  mapsncnv  6749  dfixp  6754  xpcomco  6880  xpassen  6884  ssenen  6907  undifdc  6980  unfiin  6982  fidcenumlemrks  7012  fidcenumlemr  7014  sbthlemi5  7020  sbthlemi8  7023  fi0  7034  inf00  7090  djuf1olemr  7113  djuinr  7122  djuin  7123  djuun  7126  casefun  7144  casedm  7145  caseinj  7148  caseinl  7150  caseinr  7151  endjusym  7155  eninl  7156  eninr  7157  djudm  7164  djuinj  7165  fodjuomni  7208  fodjumkv  7219  nninfwlporlemd  7231  pm54.43  7250  exmidfodomrlemim  7261  xp2dju  7275  djucomen  7276  djuassen  7277  xpdjuen  7278  pw1nel3  7291  sucpw1nel3  7293  addpiord  7376  mulpiord  7377  dmaddpi  7385  dmmulpi  7386  recmulnqg  7451  1lt2nq  7466  halfnqq  7470  dfmq0qs  7489  dfplq0qs  7490  genpdf  7568  1prl  7615  1pru  7616  ltexprlemell  7658  ltexprlemelu  7659  recexprlemell  7682  recexprlemelu  7683  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdrl  7717  cauappcvgprlem2  7720  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem2  7740  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  caucvgprprlem2  7770  addsrpr  7805  mulsrpr  7806  caucvgsrlemoffres  7860  caucvgsr  7862  suplocsrlempr  7867  addcnsr  7894  mulcnsr  7895  mulresr  7898  addvalex  7904  pitonnlem1  7905  axi2m1  7935  axcnre  7941  mulcomli  8026  mnfnre  8062  addcomli  8164  add42i  8185  mvrraddi  8236  neg0  8265  negdii  8303  negsubdi2i  8305  crap0  8977  2t2e4  9136  3t2e6  9138  3t3e9  9139  4t2e8  9140  neg1mulneg1e1  9194  8th4div3  9201  halfpm6th  9202  iap0  9205  dfdec10  9451  deceq12i  9456  numltc  9473  decsuc  9478  decsucc  9488  nummac  9492  numma2c  9493  numadd  9494  numaddc  9495  nummul1c  9496  nummul2c  9497  decma  9498  decmac  9499  decma2c  9500  decadd  9501  decaddc  9502  decrmanc  9504  decrmac  9505  decaddci  9508  decsubi  9510  decmul1  9511  decmul1c  9512  decmul2c  9513  11multnc  9515  4t3lem  9544  6t2e12  9551  7t2e14  9556  8t2e16  9562  9t2e18  9569  9t11e99  9577  halfthird  9590  5recm6rec  9591  divfnzn  9686  xnegpnf  9894  xneg0  9897  xaddmnf1  9914  xaddmnf2  9915  mnfaddpnf  9917  iooval2  9981  dfioo2  10040  fzval2  10077  fzsuc2  10145  fztpval  10149  fz0to3un2pr  10189  fz0to4untppr  10190  fzo01  10283  fzo12sn  10284  fzo0to42pr  10287  fldiv4p1lem1div2  10374  intqfrac2  10390  intfracq  10391  xnn0nnen  10508  1tonninf  10512  neg1sqe1  10705  sq2  10706  sq3  10707  cu2  10709  i2  10711  i3  10712  binom2i  10719  sq10  10783  3dec  10785  facp1  10801  fac2  10802  fac4  10804  4bc2eq6  10845  hashp1i  10881  pr0hash2ex  10886  hashfzo  10893  hashxp  10897  zfz1isolem1  10911  elovmpowrd  10955  cji  11046  cnrecnv  11054  sqrt0  11148  resqrexlemover  11154  resqrexlemcalc3  11160  absi  11203  absimle  11228  sumeq12i  11508  summodclem2a  11524  summodc  11526  sum0  11531  fsumsplitf  11551  fsum2dlemstep  11577  fsumabs  11608  fsumiun  11620  0.999...  11664  mertenslem2  11679  prodeq12i  11706  prodmodc  11721  fprod2dlemstep  11765  ege2le3  11814  eft0val  11836  cos0  11873  cos1bnd  11902  cos2bnd  11903  3dvdsdec  12006  3dvds2dec  12007  odd2np1  12014  opoe  12036  nn0o  12048  gcd0val  12097  6gcd4e2  12132  nnmindc  12171  nnminle  12172  3lcm2e6woprm  12224  3lcm2e6  12298  nn0gcdsq  12338  phiprmpw  12360  phimullem  12363  pcprecl  12427  pcprendvds  12428  pcmptdvds  12483  pockthi  12496  4sqlem13m  12541  4sqlem14  12542  4sqlem17  12545  4sqlem18  12546  4sqlem19  12547  unennn  12554  ennnfonelemj0  12558  ennnfonelem0  12562  ennnfonelem1  12564  ennnfonelemhf1o  12570  ennnfonelemrn  12576  ennnfonelemdm  12577  strnfvnd  12638  slotslfn  12644  setsfun  12653  setsfun0  12654  setscom  12658  setsslid  12669  2strstr1g  12739  eqglact  13295  ecqusaddd  13308  ghmeqker  13341  dfrhm2  13650  rmodislmod  13847  expghmap  14095  fczpsrbag  14157  cnco  14389  txuni2  14424  txbas  14426  uptx  14442  txcn  14443  cnmptid  14449  cnmpt2t  14461  xmetxp  14675  cnmetdval  14697  remetdval  14707  resubmet  14716  rerestcntop  14718  divcnap  14723  cnrehmeocntop  14764  dvexp  14860  plyun0  14882  sinhalfpilem  14926  cosneghalfpi  14933  efhalfpi  14934  cospi  14935  efipi  14936  eulerid  14937  sin2pi  14938  cos2pi  14939  ef2pi  14940  sincosq4sgn  14964  cosq14gt0  14967  tangtx  14973  sincos4thpi  14975  sincos6thpi  14977  sinkpi  14982  cosq34lt1  14985  dfrelog  14995  2logb9irr  15103  2logb9irrALT  15106  2logb9irrap  15109  zabsle1  15115  lgslem2  15117  lgsfcl2  15122  lgsdir2lem1  15144  lgsdir2lem2  15145  lgsdir2lem4  15147  lgsdir2lem5  15148  lgseisen  15190  2lgsoddprmlem3a  15195  2lgsoddprmlem3b  15196  2lgsoddprmlem3c  15197  2lgsoddprmlem3d  15198  ex-fl  15217  ex-exp  15219  ex-fac  15220  ex-bc  15221  ex-dvds  15222  ex-gcd  15223  bj-dfom  15425  012of  15486  2o01f  15487  pwle2  15489  nninfsellemqall  15505  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542  dceqnconst  15550  dcapnconst  15551  taupi  15563