Theorem eqtr4i 2255

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

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr2i  2258  3eqtr2ri  2259  3eqtr4i  2262  3eqtr4ri  2263  rabab  2824  cbvralcsf  3190  cbvrexcsf  3191  cbvrabcsf  3193  dfin5  3207  dfdif2  3208  uneqin  3458  unrab  3478  inrab  3479  inrab2  3480  difrab  3481  dfrab3ss  3485  rabun2  3486  difidALT  3564  difdifdirss  3579  dfif3  3619  tpidm  3773  dfint2  3930  iunrab  4018  uniiun  4024  intiin  4025  0iin  4029  mptv  4186  xpundi  4782  xpundir  4783  resiun2  5033  resopab  5057  mptresid  5067  dfse2  5109  cnvun  5142  cnvin  5144  imaundir  5150  imainrect  5182  cnvcnv2  5190  cnvcnvres  5200  dmtpop  5212  rnsnopg  5215  rnco2  5244  dmco  5245  co01  5251  unidmrn  5269  dfdm2  5271  funimaexg  5414  dfmpt3  5455  mptun  5464  funcocnv2  5608  fnasrn  5826  fnasrng  5828  fpr  5836  fmptap  5844  riotav  5977  dmoprab  6102  rnoprab2  6105  mpov  6111  mpomptx  6112  abrexex2g  6282  abrexex2  6286  1stval2  6318  2ndval2  6319  fo1st  6320  fo2nd  6321  xp2  6336  dfoprab4f  6356  fmpoco  6381  tposmpo  6447  recsfval  6481  frecfnom  6567  freccllem  6568  frecfcllem  6570  frecsuclem  6572  df2o3  6597  o1p1e2  6636  ecqs  6766  qliftf  6789  erovlem  6796  mapsnf1o3  6866  ixp0x  6895  xpf1o  7030  djuunr  7265  dmaddpq  7599  dmmulpq  7600  enq0enq  7651  nqprlu  7767  m1p1sr  7980  m1m1sr  7981  caucvgsr  8022  dfcnqs  8061  3m1e2  9263  2p2e4  9270  3p2e5  9285  3p3e6  9286  4p2e6  9287  4p3e7  9288  4p4e8  9289  5p2e7  9290  5p3e8  9291  5p4e9  9292  6p2e8  9293  6p3e9  9294  7p2e9  9295  nn0supp  9454  nnzrab  9503  nn0zrab  9504  dec0u  9631  dec0h  9632  decsuc  9641  decsucc  9651  numma  9654  decma  9661  decmac  9662  decma2c  9663  decadd  9664  decaddc  9665  decmul1  9674  decmul1c  9675  decmul2c  9676  5p5e10  9681  6p4e10  9682  7p3e10  9685  8p2e10  9690  5t5e25  9713  6t6e36  9718  8t6e48  9729  nn0uz  9791  nnuz  9792  xaddcom  10096  ioomax  10183  iccmax  10184  ioopos  10185  ioorp  10186  fseq1p1m1  10329  fzo0to2pr  10464  fzo0to3tp  10465  frecfzennn  10689  irec  10902  sq10e99m1  10976  facnn  10990  fac0  10991  faclbnd2  11005  zfz1isolemsplit  11103  minmax  11792  xrminmax  11827  fisumrev2  12009  fsumparts  12033  fsumiun  12040  isumnn0nn  12056  fprod2d  12186  fprodle  12203  ege2le3  12234  cos1bnd  12322  efieq1re  12335  eirraplem  12340  3dvds  12427  m1bits  12523  phiprmpw  12796  4sqlem11  12976  4sqlem19  12984  dec5dvds  12987  decsplit1  13003  unennn  13020  ennnfonelemjn  13025  qnnen  13054  strle1g  13191  quslem  13409  rmodislmod  14368  tgrest  14896  uniretop  15252  cnfldtopn  15266  dvexp  15438  dvef  15454  elply2  15462  cospi  15527  sincos6thpi  15569  lgsdir2lem2  15761  lgsquadlem2  15810  lgsquad2lem2  15814  2lgsoddprmlem3c  15841  bj-omind  16546  gfsump1  16703