Theorem eqtr4i 2163

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

Syntax hints:   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  3eqtr2i  2166  3eqtr2ri  2167  3eqtr4i  2170  3eqtr4ri  2171  rabab  2707  cbvralcsf  3062  cbvrexcsf  3063  cbvrabcsf  3065  dfin5  3078  dfdif2  3079  uneqin  3327  unrab  3347  inrab  3348  inrab2  3349  difrab  3350  dfrab3ss  3354  rabun2  3355  difidALT  3432  difdifdirss  3447  dfif3  3487  tpidm  3625  dfint2  3773  iunrab  3860  uniiun  3866  intiin  3867  0iin  3871  mptv  4025  xpundi  4595  xpundir  4596  resiun2  4839  resopab  4863  opabresid  4872  dfse2  4912  cnvun  4944  cnvin  4946  imaundir  4952  imainrect  4984  cnvcnv2  4992  cnvcnvres  5002  dmtpop  5014  rnsnopg  5017  rnco2  5046  dmco  5047  co01  5053  unidmrn  5071  dfdm2  5073  funimaexg  5207  dfmpt3  5245  mptun  5254  funcocnv2  5392  fnasrn  5598  fnasrng  5600  fpr  5602  fmptap  5610  riotav  5735  dmoprab  5852  rnoprab2  5855  mpov  5861  mpomptx  5862  abrexex2g  6018  abrexex2  6022  1stval2  6053  2ndval2  6054  fo1st  6055  fo2nd  6056  xp2  6071  dfoprab4f  6091  fmpoco  6113  tposmpo  6178  recsfval  6212  frecfnom  6298  freccllem  6299  frecfcllem  6301  frecsuclem  6303  df2o3  6327  o1p1e2  6364  ecqs  6491  qliftf  6514  erovlem  6521  mapsnf1o3  6591  ixp0x  6620  xpf1o  6738  djuunr  6951  dmaddpq  7187  dmmulpq  7188  enq0enq  7239  nqprlu  7355  m1p1sr  7568  m1m1sr  7569  caucvgsr  7610  dfcnqs  7649  3m1e2  8840  2p2e4  8847  3p2e5  8861  3p3e6  8862  4p2e6  8863  4p3e7  8864  4p4e8  8865  5p2e7  8866  5p3e8  8867  5p4e9  8868  6p2e8  8869  6p3e9  8870  7p2e9  8871  nn0supp  9029  nnzrab  9078  nn0zrab  9079  dec0u  9202  dec0h  9203  decsuc  9212  decsucc  9222  numma  9225  decma  9232  decmac  9233  decma2c  9234  decadd  9235  decaddc  9236  decmul1  9245  decmul1c  9246  decmul2c  9247  5p5e10  9252  6p4e10  9253  7p3e10  9256  8p2e10  9261  5t5e25  9284  6t6e36  9289  8t6e48  9300  nn0uz  9360  nnuz  9361  xaddcom  9644  ioomax  9731  iccmax  9732  ioopos  9733  ioorp  9734  fseq1p1m1  9874  fzo0to2pr  9995  fzo0to3tp  9996  frecfzennn  10199  irec  10392  sq10e99m1  10460  facnn  10473  fac0  10474  faclbnd2  10488  zfz1isolemsplit  10581  minmax  11001  xrminmax  11034  fisumrev2  11215  fsumparts  11239  fsumiun  11246  isumnn0nn  11262  ege2le3  11377  cos1bnd  11466  efieq1re  11478  eirraplem  11483  phiprmpw  11898  unennn  11910  ennnfonelemjn  11915  qnnen  11944  strle1g  12049  tgrest  12338  uniretop  12694  dvexp  12844  dvef  12856  cospi  12881  sincos6thpi  12923  bj-omind  13132