Theorem eqtri 2373

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

Hypotheses

Ref	Expression
eqtri.1	⊢ A = B
eqtri.2	⊢ B = C

Assertion

Ref	Expression
eqtri	⊢ A = C

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 ⊢ A = B
2		eqtri.2	. . 3 ⊢ B = C
3	2	eqeq2i 2363	. 2 ⊢ (A = B ↔ A = C)
4	1, 3	mpbi 199	1 ⊢ A = C

Syntax hints:   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  eqtr2i  2374  eqtr3i  2375  eqtr4i  2376  3eqtri  2377  3eqtrri  2378  3eqtr2i  2379  cbvrab  2858  csb2  3139  cbvrabcsf  3202  difeq1  3247  difeq2  3248  symdifeq1  3249  symdifeq2  3250  difeq12i  3384  inrot  3471  dfun3  3494  dfin3  3495  invdif  3497  difundi  3508  difindi  3510  symdif1  3520  rabnc  3575  undif1  3626  ssdifin0  3632  dfif2  3665  dfif3  3673  dfif4  3674  dfif5  3675  ifbieq2i  3682  ifbieq12i  3684  pwjust  3724  snjust  3741  dfpr2  3750  difprsn1  3848  diftpsn3  3850  sspr  3870  sstp  3871  dfuni2  3894  intab  3957  intunsn  3966  rint0  3967  iunid  4022  viin  4026  iinrab  4029  iinrab2  4030  2iunin  4035  riin0  4040  uncompl  4075  inindif  4076  cokeq12i  4237  xpkexg  4289  pw1eqadj  4333  iotajust  4339  dfiota2  4341  dfiota4  4373  addcid1  4406  addcid2  4408  nnc0suc  4413  addc6  4419  nncaddccl  4420  nnsucelrlem3  4427  addcnnul  4454  ltfintr  4460  ltfintrilem1  4466  ncfinraise  4482  tfinnul  4492  tfinsuc  4499  tfin1c  4500  sucoddeven  4512  dfevenfin2  4513  dfoddfin2  4514  evenodddisj  4517  oddtfin  4519  nnadjoin  4521  sfindbl  4531  spfinex  4538  opeq12i  4584  phiun  4615  phialllem1  4617  phialllem2  4618  unopab  4639  dfid3  4769  elxpi  4801  csbxpg  4814  fconstopab  4816  inxp  4864  coeq12i  4881  dfrn3  4904  dmopab  4916  dmopab3  4918  dmxpin  4926  reseq12i  4933  dfima4  4953  rnopab  4968  rncoss  4973  rncoeq  4976  resundi  4982  resindi  4984  resopab  5000  resima2  5008  imadisj  5016  iniseg  5023  ndmima  5026  cnvin  5036  rnun  5037  imaundi  5040  cnvxp  5044  rnxp  5052  rnxpss  5054  dminxp  5062  dmpropg  5069  op1sta  5073  opswap  5075  op2nda  5077  resdmres  5079  coundi  5083  coundir  5084  funi  5138  funcnvuni  5162  funcnvres  5166  fnresdisj  5194  fv2  5325  dfimafn2  5368  fnimapr  5375  ressnop0  5437  fpr  5438  fvsnun1  5448  imauni  5466  rnsi  5522  resoprab  5582  ov  5596  ovigg  5597  ovg  5602  caov31  5638  caov42  5642  caovdilem  5644  caovmo  5646  cbvmpt  5677  mptpreima  5683  dmmpt  5684  dmmptss  5686  rnmpt  5687  mptfng  5689  fvmptg  5699  fvmpts  5702  fvmpt2i  5704  ovmpt4g  5711  ovmpt2x  5713  ovmpt2ga  5714  rnmpt2  5718  mptresid  5721  fvmptex  5722  f1od  5727  composefn  5819  cnvpprod  5842  rnpprod  5843  fvfullfun  5865  clos1conn  5880  clos1induct  5881  clos1basesuc  5883  dfec2  5949  ecidsn  5974  ecid  5990  pmvalg  6011  mapsn  6027  enadj  6061  nenpw1pwlem1  6085  mucnc  6132  mucass  6136  muc0  6143  1p1e2c  6156  2p1e3c  6157  tc2c  6167  fnce  6177  ce2  6193  ce2nc1  6194  ce2ncpw11c  6195  sbthlem1  6204  leconnnc  6219  tcfnex  6245  addcdi  6251  nmembers1lem1  6269  nmembers1  6272  nncdiv3  6278  nnc3n3p1  6279  nnc3n3p2  6280  nchoicelem2  6291  nchoicelem17  6306  frecexg  6313  dmfrec  6317  fnfreclem2  6319  fnfreclem3  6320  frec0  6322  frecsuc  6323