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  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  11795  xrminmax  11830  fisumrev2  12012  fsumparts  12036  fsumiun  12043  isumnn0nn  12059  fprod2d  12189  fprodle  12206  ege2le3  12237  cos1bnd  12325  efieq1re  12338  eirraplem  12343  3dvds  12430  m1bits  12526  phiprmpw  12799  4sqlem11  12979  4sqlem19  12987  dec5dvds  12990  decsplit1  13006  unennn  13023  ennnfonelemjn  13028  qnnen  13057  strle1g  13194  quslem  13412  rmodislmod  14371  tgrest  14899  uniretop  15255  cnfldtopn  15269  dvexp  15441  dvef  15457  elply2  15465  cospi  15530  sincos6thpi  15572  lgsdir2lem2  15764  lgsquadlem2  15813  lgsquad2lem2  15817  2lgsoddprmlem3c  15844  bj-omind  16555  gfsump1  16713