Theorem eqtr4i 2255

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr4i.1	⊢ 𝐴 = 𝐵
eqtr4i.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eqtr4i	⊢ 𝐴 = 𝐶

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtr4i.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2235	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2252	1 ⊢ 𝐴 = 𝐶

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  5825  fnasrng  5827  fpr  5835  fmptap  5843  riotav  5976  dmoprab  6101  rnoprab2  6104  mpov  6110  mpomptx  6111  abrexex2g  6281  abrexex2  6285  1stval2  6317  2ndval2  6318  fo1st  6319  fo2nd  6320  xp2  6335  dfoprab4f  6355  fmpoco  6380  tposmpo  6446  recsfval  6480  frecfnom  6566  freccllem  6567  frecfcllem  6569  frecsuclem  6571  df2o3  6596  o1p1e2  6635  ecqs  6765  qliftf  6788  erovlem  6795  mapsnf1o3  6865  ixp0x  6894  xpf1o  7029  djuunr  7264  dmaddpq  7598  dmmulpq  7599  enq0enq  7650  nqprlu  7766  m1p1sr  7979  m1m1sr  7980  caucvgsr  8021  dfcnqs  8060  3m1e2  9262  2p2e4  9269  3p2e5  9284  3p3e6  9285  4p2e6  9286  4p3e7  9287  4p4e8  9288  5p2e7  9289  5p3e8  9290  5p4e9  9291  6p2e8  9292  6p3e9  9293  7p2e9  9294  nn0supp  9453  nnzrab  9502  nn0zrab  9503  dec0u  9630  dec0h  9631  decsuc  9640  decsucc  9650  numma  9653  decma  9660  decmac  9661  decma2c  9662  decadd  9663  decaddc  9664  decmul1  9673  decmul1c  9674  decmul2c  9675  5p5e10  9680  6p4e10  9681  7p3e10  9684  8p2e10  9689  5t5e25  9712  6t6e36  9717  8t6e48  9728  nn0uz  9790  nnuz  9791  xaddcom  10095  ioomax  10182  iccmax  10183  ioopos  10184  ioorp  10185  fseq1p1m1  10328  fzo0to2pr  10462  fzo0to3tp  10463  frecfzennn  10687  irec  10900  sq10e99m1  10974  facnn  10988  fac0  10989  faclbnd2  11003  zfz1isolemsplit  11101  minmax  11790  xrminmax  11825  fisumrev2  12006  fsumparts  12030  fsumiun  12037  isumnn0nn  12053  fprod2d  12183  fprodle  12200  ege2le3  12231  cos1bnd  12319  efieq1re  12332  eirraplem  12337  3dvds  12424  m1bits  12520  phiprmpw  12793  4sqlem11  12973  4sqlem19  12981  dec5dvds  12984  decsplit1  13000  unennn  13017  ennnfonelemjn  13022  qnnen  13051  strle1g  13188  quslem  13406  rmodislmod  14364  tgrest  14892  uniretop  15248  cnfldtopn  15262  dvexp  15434  dvef  15450  elply2  15458  cospi  15523  sincos6thpi  15565  lgsdir2lem2  15757  lgsquadlem2  15806  lgsquad2lem2  15810  2lgsoddprmlem3c  15837  bj-omind  16529