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  2759  cbvralcsf  3120  cbvrexcsf  3121  cbvrabcsf  3123  dfin5  3137  dfdif2  3138  uneqin  3387  unrab  3407  inrab  3408  inrab2  3409  difrab  3410  dfrab3ss  3414  rabun2  3415  difidALT  3493  difdifdirss  3508  dfif3  3548  tpidm  3695  dfint2  3847  iunrab  3935  uniiun  3941  intiin  3942  0iin  3946  mptv  4101  xpundi  4683  xpundir  4684  resiun2  4928  resopab  4952  opabresid  4961  dfse2  5002  cnvun  5035  cnvin  5037  imaundir  5043  imainrect  5075  cnvcnv2  5083  cnvcnvres  5093  dmtpop  5105  rnsnopg  5108  rnco2  5137  dmco  5138  co01  5144  unidmrn  5162  dfdm2  5164  funimaexg  5301  dfmpt3  5339  mptun  5348  funcocnv2  5487  fnasrn  5695  fnasrng  5697  fpr  5699  fmptap  5707  riotav  5836  dmoprab  5956  rnoprab2  5959  mpov  5965  mpomptx  5966  abrexex2g  6121  abrexex2  6125  1stval2  6156  2ndval2  6157  fo1st  6158  fo2nd  6159  xp2  6174  dfoprab4f  6194  fmpoco  6217  tposmpo  6282  recsfval  6316  frecfnom  6402  freccllem  6403  frecfcllem  6405  frecsuclem  6407  df2o3  6431  o1p1e2  6469  ecqs  6597  qliftf  6620  erovlem  6627  mapsnf1o3  6697  ixp0x  6726  xpf1o  6844  djuunr  7065  dmaddpq  7378  dmmulpq  7379  enq0enq  7430  nqprlu  7546  m1p1sr  7759  m1m1sr  7760  caucvgsr  7801  dfcnqs  7840  3m1e2  9039  2p2e4  9046  3p2e5  9060  3p3e6  9061  4p2e6  9062  4p3e7  9063  4p4e8  9064  5p2e7  9065  5p3e8  9066  5p4e9  9067  6p2e8  9068  6p3e9  9069  7p2e9  9070  nn0supp  9228  nnzrab  9277  nn0zrab  9278  dec0u  9404  dec0h  9405  decsuc  9414  decsucc  9424  numma  9427  decma  9434  decmac  9435  decma2c  9436  decadd  9437  decaddc  9438  decmul1  9447  decmul1c  9448  decmul2c  9449  5p5e10  9454  6p4e10  9455  7p3e10  9458  8p2e10  9463  5t5e25  9486  6t6e36  9491  8t6e48  9502  nn0uz  9562  nnuz  9563  xaddcom  9861  ioomax  9948  iccmax  9949  ioopos  9950  ioorp  9951  fseq1p1m1  10094  fzo0to2pr  10218  fzo0to3tp  10219  frecfzennn  10426  irec  10620  sq10e99m1  10693  facnn  10707  fac0  10708  faclbnd2  10722  zfz1isolemsplit  10818  minmax  11238  xrminmax  11273  fisumrev2  11454  fsumparts  11478  fsumiun  11485  isumnn0nn  11501  fprod2d  11631  fprodle  11648  ege2le3  11679  cos1bnd  11767  efieq1re  11779  eirraplem  11784  phiprmpw  12222  unennn  12398  ennnfonelemjn  12403  qnnen  12432  strle1g  12565  quslem  12745  rmodislmod  13441  tgrest  13672  uniretop  14028  dvexp  14178  dvef  14191  cospi  14224  sincos6thpi  14266  lgsdir2lem2  14433  2lgsoddprmlem3c  14460  bj-omind  14689