Theorem eqtr4i 2201

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

Syntax hints:   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  3eqtr2i  2204  3eqtr2ri  2205  3eqtr4i  2208  3eqtr4ri  2209  rabab  2758  cbvralcsf  3119  cbvrexcsf  3120  cbvrabcsf  3122  dfin5  3136  dfdif2  3137  uneqin  3386  unrab  3406  inrab  3407  inrab2  3408  difrab  3409  dfrab3ss  3413  rabun2  3414  difidALT  3492  difdifdirss  3507  dfif3  3547  tpidm  3694  dfint2  3846  iunrab  3934  uniiun  3940  intiin  3941  0iin  3945  mptv  4100  xpundi  4682  xpundir  4683  resiun2  4927  resopab  4951  opabresid  4960  dfse2  5001  cnvun  5034  cnvin  5036  imaundir  5042  imainrect  5074  cnvcnv2  5082  cnvcnvres  5092  dmtpop  5104  rnsnopg  5107  rnco2  5136  dmco  5137  co01  5143  unidmrn  5161  dfdm2  5163  funimaexg  5300  dfmpt3  5338  mptun  5347  funcocnv2  5486  fnasrn  5694  fnasrng  5696  fpr  5698  fmptap  5706  riotav  5835  dmoprab  5955  rnoprab2  5958  mpov  5964  mpomptx  5965  abrexex2g  6120  abrexex2  6124  1stval2  6155  2ndval2  6156  fo1st  6157  fo2nd  6158  xp2  6173  dfoprab4f  6193  fmpoco  6216  tposmpo  6281  recsfval  6315  frecfnom  6401  freccllem  6402  frecfcllem  6404  frecsuclem  6406  df2o3  6430  o1p1e2  6468  ecqs  6596  qliftf  6619  erovlem  6626  mapsnf1o3  6696  ixp0x  6725  xpf1o  6843  djuunr  7064  dmaddpq  7377  dmmulpq  7378  enq0enq  7429  nqprlu  7545  m1p1sr  7758  m1m1sr  7759  caucvgsr  7800  dfcnqs  7839  3m1e2  9037  2p2e4  9044  3p2e5  9058  3p3e6  9059  4p2e6  9060  4p3e7  9061  4p4e8  9062  5p2e7  9063  5p3e8  9064  5p4e9  9065  6p2e8  9066  6p3e9  9067  7p2e9  9068  nn0supp  9226  nnzrab  9275  nn0zrab  9276  dec0u  9402  dec0h  9403  decsuc  9412  decsucc  9422  numma  9425  decma  9432  decmac  9433  decma2c  9434  decadd  9435  decaddc  9436  decmul1  9445  decmul1c  9446  decmul2c  9447  5p5e10  9452  6p4e10  9453  7p3e10  9456  8p2e10  9461  5t5e25  9484  6t6e36  9489  8t6e48  9500  nn0uz  9560  nnuz  9561  xaddcom  9859  ioomax  9946  iccmax  9947  ioopos  9948  ioorp  9949  fseq1p1m1  10091  fzo0to2pr  10215  fzo0to3tp  10216  frecfzennn  10423  irec  10616  sq10e99m1  10688  facnn  10702  fac0  10703  faclbnd2  10717  zfz1isolemsplit  10813  minmax  11233  xrminmax  11268  fisumrev2  11449  fsumparts  11473  fsumiun  11480  isumnn0nn  11496  fprod2d  11626  fprodle  11643  ege2le3  11674  cos1bnd  11762  efieq1re  11774  eirraplem  11779  phiprmpw  12216  unennn  12392  ennnfonelemjn  12397  qnnen  12426  strle1g  12559  tgrest  13562  uniretop  13918  dvexp  14068  dvef  14081  cospi  14114  sincos6thpi  14156  lgsdir2lem2  14323  bj-omind  14568