Theorem eqtr4i 2376

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

Hypotheses

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

Assertion

Ref	Expression
eqtr4i	⊢ A = C

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 ⊢ A = B
2		eqtr4i.2	. . 3 ⊢ C = B
3	2	eqcomi 2357	. 2 ⊢ B = C
4	1, 3	eqtri 2373	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:  3eqtr2i  2379  3eqtr2ri  2380  3eqtr4i  2383  3eqtr4ri  2384  rabab  2876  cbvralcsf  3198  cbvrabcsf  3201  dfdif2  3222  rabbi2dva  3463  uneqin  3506  unrab  3526  inrab  3527  inrab2  3528  difrab  3529  dfrab3ss  3533  rabun2  3534  rabxm  3573  difidALT  3619  difdifdir  3637  dfif3  3672  dfif5  3674  tpidm  3824  ssunpr  3868  sstp  3870  dfint2  3928  iunrab  4013  uniiun  4019  intiin  4020  0iin  4024  complV  4070  dfaddc2  4381  dfnnc2  4395  preaddccan2lem1  4454  ltfinex  4464  evenfinex  4503  oddfinex  4504  tfinnn  4534  spfinex  4537  dfop2  4575  dfproj12  4576  dfproj22  4577  phiall  4618  opeq  4619  dfima2  4745  xpundi  4832  xpundir  4833  dmun  4912  rnopab2  4968  resopab  4999  opabresid  5003  cnvun  5033  imaundir  5040  dmtpop  5071  rnco2  5088  dmco  5089  f1ococnv2  5309  dmoprab  5574  rnoprab2  5577  fnov  5591  fconstmpt  5681  dmmpt  5683  mpt2mptx  5708  mptv  5718  mpt2v  5719  dfswap3  5728  dfswap4  5729  releqmpt  5808  releqmpt2  5809  cupex  5816  composeex  5820  disjex  5823  addcfnex  5824  funsex  5828  fnsex  5832  crossex  5850  pw1fnex  5852  pw1fnf1o  5855  domfnex  5870  ranfnex  5871  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  qsexg  5982  ecqs  5988  enex  6031  enpw1pw  6075  enprmaplem1  6076  enprmaplem4  6079  mucex  6133  ncpw1c  6154  ceex  6174  ce0  6190  ce2  6192  leconnnc  6218  tcncv  6226  tce2  6236  tcfnex  6244  nmembers1lem1  6268