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  2877  cbvralcsf  3199  cbvrabcsf  3202  dfdif2  3223  rabbi2dva  3464  uneqin  3507  unrab  3527  inrab  3528  inrab2  3529  difrab  3530  dfrab3ss  3534  rabun2  3535  rabxm  3574  difidALT  3620  difdifdir  3638  dfif3  3673  dfif5  3675  tpidm  3825  ssunpr  3869  sstp  3871  dfint2  3929  iunrab  4014  uniiun  4020  intiin  4021  0iin  4025  complV  4071  dfaddc2  4382  dfnnc2  4396  preaddccan2lem1  4455  ltfinex  4465  evenfinex  4504  oddfinex  4505  tfinnn  4535  spfinex  4538  dfop2  4576  dfproj12  4577  dfproj22  4578  phiall  4619  opeq  4620  dfima2  4746  xpundi  4833  xpundir  4834  dmun  4913  rnopab2  4969  resopab  5000  opabresid  5004  cnvun  5034  imaundir  5041  dmtpop  5072  rnco2  5089  dmco  5090  f1ococnv2  5310  dmoprab  5575  rnoprab2  5578  fnov  5592  fconstmpt  5682  dmmpt  5684  mpt2mptx  5709  mptv  5719  mpt2v  5720  dfswap3  5729  dfswap4  5730  releqmpt  5809  releqmpt2  5810  cupex  5817  composeex  5821  disjex  5824  addcfnex  5825  funsex  5829  fnsex  5833  crossex  5851  pw1fnex  5853  pw1fnf1o  5856  domfnex  5871  ranfnex  5872  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  qsexg  5983  ecqs  5989  enex  6032  enpw1pw  6076  enprmaplem1  6077  enprmaplem4  6080  mucex  6134  ncpw1c  6155  ceex  6175  ce0  6191  ce2  6193  leconnnc  6219  tcncv  6227  tce2  6237  tcfnex  6245  nmembers1lem1  6269