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  2857  csb2  3138  cbvrabcsf  3201  difeq1  3246  difeq2  3247  symdifeq1  3248  symdifeq2  3249  difeq12i  3383  inrot  3470  dfun3  3493  dfin3  3494  invdif  3496  difundi  3507  difindi  3509  symdif1  3519  rabnc  3574  undif1  3625  ssdifin0  3631  dfif2  3664  dfif3  3672  dfif4  3673  dfif5  3674  ifbieq2i  3681  ifbieq12i  3683  pwjust  3723  snjust  3740  dfpr2  3749  difprsn1  3847  diftpsn3  3849  sspr  3869  sstp  3870  dfuni2  3893  intab  3956  intunsn  3965  rint0  3966  iunid  4021  viin  4025  iinrab  4028  iinrab2  4029  2iunin  4034  riin0  4039  uncompl  4074  inindif  4075  cokeq12i  4236  xpkexg  4288  pw1eqadj  4332  iotajust  4338  dfiota2  4340  dfiota4  4372  addcid1  4405  addcid2  4407  nnc0suc  4412  addc6  4418  nncaddccl  4419  nnsucelrlem3  4426  addcnnul  4453  ltfintr  4459  ltfintrilem1  4465  ncfinraise  4481  tfinnul  4491  tfinsuc  4498  tfin1c  4499  sucoddeven  4511  dfevenfin2  4512  dfoddfin2  4513  evenodddisj  4516  oddtfin  4518  nnadjoin  4520  sfindbl  4530  spfinex  4537  opeq12i  4583  phiun  4614  phialllem1  4616  phialllem2  4617  unopab  4638  dfid3  4768  elxpi  4800  csbxpg  4813  fconstopab  4815  inxp  4863  coeq12i  4880  dfrn3  4903  dmopab  4915  dmopab3  4917  dmxpin  4925  reseq12i  4932  dfima4  4952  rnopab  4967  rncoss  4972  rncoeq  4975  resundi  4981  resindi  4983  resopab  4999  resima2  5007  imadisj  5015  iniseg  5022  ndmima  5025  cnvin  5035  rnun  5036  imaundi  5039  cnvxp  5043  rnxp  5051  rnxpss  5053  dminxp  5061  dmpropg  5068  op1sta  5072  opswap  5074  op2nda  5076  resdmres  5078  coundi  5082  coundir  5083  funi  5137  funcnvuni  5161  funcnvres  5165  fnresdisj  5193  fv2  5324  dfimafn2  5367  fnimapr  5374  ressnop0  5436  fpr  5437  fvsnun1  5447  imauni  5465  rnsi  5521  resoprab  5581  ov  5595  ovigg  5596  ovg  5601  caov31  5637  caov42  5641  caovdilem  5643  caovmo  5645  cbvmpt  5676  mptpreima  5682  dmmpt  5683  dmmptss  5685  rnmpt  5686  mptfng  5688  fvmptg  5698  fvmpts  5701  fvmpt2i  5703  ovmpt4g  5710  ovmpt2x  5712  ovmpt2ga  5713  rnmpt2  5717  mptresid  5720  fvmptex  5721  f1od  5726  composefn  5818  cnvpprod  5841  rnpprod  5842  fvfullfun  5864  clos1conn  5879  clos1induct  5880  clos1basesuc  5882  dfec2  5948  ecidsn  5973  ecid  5989  pmvalg  6010  mapsn  6026  enadj  6060  nenpw1pwlem1  6084  mucnc  6131  mucass  6135  muc0  6142  1p1e2c  6155  2p1e3c  6156  tc2c  6166  fnce  6176  ce2  6192  ce2nc1  6193  ce2ncpw11c  6194  sbthlem1  6203  leconnnc  6218  tcfnex  6244  addcdi  6250  nmembers1lem1  6268  nmembers1  6271  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  nchoicelem2  6290  nchoicelem17  6305  frecexg  6312  dmfrec  6316  fnfreclem2  6318  fnfreclem3  6319  frec0  6321  frecsuc  6322