Theorem eqtr4i 2256

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 2236	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2253	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  3eqtr2i  2259  3eqtr2ri  2260  3eqtr4i  2263  3eqtr4ri  2264  rabab  2835  cbvralcsf  3201  cbvrexcsf  3202  cbvrabcsf  3204  dfin5  3218  dfdif2  3219  uneqin  3472  unrab  3492  inrab  3493  inrab2  3494  difrab  3495  dfrab3ss  3499  rabun2  3500  difidALT  3578  difdifdirss  3594  dfif3  3636  tpidm  3793  dfint2  3951  iunrab  4039  uniiun  4045  intiin  4046  0iin  4050  mptv  4207  xpundi  4806  xpundir  4807  resiun2  5058  resopab  5082  mptresid  5092  dfse2  5135  cnvun  5168  cnvin  5170  imaundir  5176  imainrect  5208  cnvcnv2  5216  cnvcnvres  5226  dmtpop  5238  rnsnopg  5241  rnco2  5270  dmco  5271  co01  5277  unidmrn  5295  dfdm2  5297  funimaexg  5440  dfmpt3  5481  mptun  5490  funcocnv2  5639  fnasrn  5856  fnasrng  5858  fpr  5866  fmptap  5874  riotav  6009  dmoprab  6134  rnoprab2  6137  mpov  6143  mpomptx  6144  abrexex2g  6313  abrexex2  6317  1stval2  6349  2ndval2  6350  fo1st  6351  fo2nd  6352  xp2  6367  dfoprab4f  6387  fmpoco  6412  tposmpo  6512  recsfval  6546  frecfnom  6632  freccllem  6633  frecfcllem  6635  frecsuclem  6637  df2o3  6662  o1p1e2  6701  ecqs  6831  qliftf  6854  erovlem  6861  mapsnf1o3  6932  ixp0x  6961  xpf1o  7097  djuunr  7357  dmaddpq  7694  dmmulpq  7695  enq0enq  7746  nqprlu  7862  m1p1sr  8075  m1m1sr  8076  caucvgsr  8117  dfcnqs  8156  3m1e2  9357  2p2e4  9364  3p2e5  9379  3p3e6  9380  4p2e6  9381  4p3e7  9382  4p4e8  9383  5p2e7  9384  5p3e8  9385  5p4e9  9386  6p2e8  9387  6p3e9  9388  7p2e9  9389  nn0supp  9552  nnzrab  9601  nn0zrab  9602  dec0u  9729  dec0h  9730  decsuc  9739  decsucc  9749  numma  9752  decma  9759  decmac  9760  decma2c  9761  decadd  9762  decaddc  9763  decmul1  9772  decmul1c  9773  decmul2c  9774  5p5e10  9779  6p4e10  9780  7p3e10  9783  8p2e10  9788  5t5e25  9811  6t6e36  9816  8t6e48  9827  nn0uz  9889  nnuz  9890  xaddcom  10194  ioomax  10281  iccmax  10282  ioopos  10283  ioorp  10284  fseq1p1m1  10428  fzo0to2pr  10563  fzo0to3tp  10564  frecfzennn  10788  irec  11001  sq10e99m1  11075  facnn  11089  fac0  11090  faclbnd2  11104  zfz1isolemsplit  11210  minmax  11915  xrminmax  11950  fisumrev2  12132  fsumparts  12156  fsumiun  12163  isumnn0nn  12179  fprod2d  12309  fprodle  12326  ege2le3  12357  cos1bnd  12445  efieq1re  12458  eirraplem  12463  3dvds  12550  m1bits  12646  phiprmpw  12919  4sqlem11  13099  4sqlem19  13107  dec5dvds  13110  decsplit1  13126  unennn  13148  ennnfonelemjn  13153  qnnen  13182  strle1g  13319  quslem  13537  rmodislmod  14499  tgrest  15034  uniretop  15390  cnfldtopn  15404  dvexp  15576  dvef  15592  elply2  15600  cospi  15665  sincos6thpi  15707  lgsdir2lem2  15902  lgsquadlem2  15951  lgsquad2lem2  15955  2lgsoddprmlem3c  15982  konigsbergumgr  16482  konigsberglem1  16483  konigsberglem2  16484  bj-omind  16704  gfsump1  16868