Theorem eqtr4i 2194

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 2174	. 2 |- B = C
4	1, 3	eqtri 2191	1 |- A = C

Syntax hints:   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  3eqtr2i  2197  3eqtr2ri  2198  3eqtr4i  2201  3eqtr4ri  2202  rabab  2751  cbvralcsf  3111  cbvrexcsf  3112  cbvrabcsf  3114  dfin5  3128  dfdif2  3129  uneqin  3378  unrab  3398  inrab  3399  inrab2  3400  difrab  3401  dfrab3ss  3405  rabun2  3406  difidALT  3484  difdifdirss  3499  dfif3  3539  tpidm  3685  dfint2  3833  iunrab  3920  uniiun  3926  intiin  3927  0iin  3931  mptv  4086  xpundi  4667  xpundir  4668  resiun2  4911  resopab  4935  opabresid  4944  dfse2  4984  cnvun  5016  cnvin  5018  imaundir  5024  imainrect  5056  cnvcnv2  5064  cnvcnvres  5074  dmtpop  5086  rnsnopg  5089  rnco2  5118  dmco  5119  co01  5125  unidmrn  5143  dfdm2  5145  funimaexg  5282  dfmpt3  5320  mptun  5329  funcocnv2  5467  fnasrn  5674  fnasrng  5676  fpr  5678  fmptap  5686  riotav  5814  dmoprab  5934  rnoprab2  5937  mpov  5943  mpomptx  5944  abrexex2g  6099  abrexex2  6103  1stval2  6134  2ndval2  6135  fo1st  6136  fo2nd  6137  xp2  6152  dfoprab4f  6172  fmpoco  6195  tposmpo  6260  recsfval  6294  frecfnom  6380  freccllem  6381  frecfcllem  6383  frecsuclem  6385  df2o3  6409  o1p1e2  6447  ecqs  6575  qliftf  6598  erovlem  6605  mapsnf1o3  6675  ixp0x  6704  xpf1o  6822  djuunr  7043  dmaddpq  7341  dmmulpq  7342  enq0enq  7393  nqprlu  7509  m1p1sr  7722  m1m1sr  7723  caucvgsr  7764  dfcnqs  7803  3m1e2  8998  2p2e4  9005  3p2e5  9019  3p3e6  9020  4p2e6  9021  4p3e7  9022  4p4e8  9023  5p2e7  9024  5p3e8  9025  5p4e9  9026  6p2e8  9027  6p3e9  9028  7p2e9  9029  nn0supp  9187  nnzrab  9236  nn0zrab  9237  dec0u  9363  dec0h  9364  decsuc  9373  decsucc  9383  numma  9386  decma  9393  decmac  9394  decma2c  9395  decadd  9396  decaddc  9397  decmul1  9406  decmul1c  9407  decmul2c  9408  5p5e10  9413  6p4e10  9414  7p3e10  9417  8p2e10  9422  5t5e25  9445  6t6e36  9450  8t6e48  9461  nn0uz  9521  nnuz  9522  xaddcom  9818  ioomax  9905  iccmax  9906  ioopos  9907  ioorp  9908  fseq1p1m1  10050  fzo0to2pr  10174  fzo0to3tp  10175  frecfzennn  10382  irec  10575  sq10e99m1  10647  facnn  10661  fac0  10662  faclbnd2  10676  zfz1isolemsplit  10773  minmax  11193  xrminmax  11228  fisumrev2  11409  fsumparts  11433  fsumiun  11440  isumnn0nn  11456  fprod2d  11586  fprodle  11603  ege2le3  11634  cos1bnd  11722  efieq1re  11734  eirraplem  11739  phiprmpw  12176  unennn  12352  ennnfonelemjn  12357  qnnen  12386  strle1g  12508  tgrest  12963  uniretop  13319  dvexp  13469  dvef  13482  cospi  13515  sincos6thpi  13557  lgsdir2lem2  13724  bj-omind  13969