Theorem eqtr4i 2253

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr2i  2256  3eqtr2ri  2257  3eqtr4i  2260  3eqtr4ri  2261  rabab  2822  cbvralcsf  3188  cbvrexcsf  3189  cbvrabcsf  3191  dfin5  3205  dfdif2  3206  uneqin  3456  unrab  3476  inrab  3477  inrab2  3478  difrab  3479  dfrab3ss  3483  rabun2  3484  difidALT  3562  difdifdirss  3577  dfif3  3617  tpidm  3771  dfint2  3928  iunrab  4016  uniiun  4022  intiin  4023  0iin  4027  mptv  4184  xpundi  4780  xpundir  4781  resiun2  5031  resopab  5055  mptresid  5065  dfse2  5107  cnvun  5140  cnvin  5142  imaundir  5148  imainrect  5180  cnvcnv2  5188  cnvcnvres  5198  dmtpop  5210  rnsnopg  5213  rnco2  5242  dmco  5243  co01  5249  unidmrn  5267  dfdm2  5269  funimaexg  5411  dfmpt3  5452  mptun  5461  funcocnv2  5605  fnasrn  5821  fnasrng  5823  fpr  5831  fmptap  5839  riotav  5972  dmoprab  6097  rnoprab2  6100  mpov  6106  mpomptx  6107  abrexex2g  6277  abrexex2  6281  1stval2  6313  2ndval2  6314  fo1st  6315  fo2nd  6316  xp2  6331  dfoprab4f  6351  fmpoco  6376  tposmpo  6442  recsfval  6476  frecfnom  6562  freccllem  6563  frecfcllem  6565  frecsuclem  6567  df2o3  6592  o1p1e2  6631  ecqs  6761  qliftf  6784  erovlem  6791  mapsnf1o3  6861  ixp0x  6890  xpf1o  7025  djuunr  7256  dmaddpq  7589  dmmulpq  7590  enq0enq  7641  nqprlu  7757  m1p1sr  7970  m1m1sr  7971  caucvgsr  8012  dfcnqs  8051  3m1e2  9253  2p2e4  9260  3p2e5  9275  3p3e6  9276  4p2e6  9277  4p3e7  9278  4p4e8  9279  5p2e7  9280  5p3e8  9281  5p4e9  9282  6p2e8  9283  6p3e9  9284  7p2e9  9285  nn0supp  9444  nnzrab  9493  nn0zrab  9494  dec0u  9621  dec0h  9622  decsuc  9631  decsucc  9641  numma  9644  decma  9651  decmac  9652  decma2c  9653  decadd  9654  decaddc  9655  decmul1  9664  decmul1c  9665  decmul2c  9666  5p5e10  9671  6p4e10  9672  7p3e10  9675  8p2e10  9680  5t5e25  9703  6t6e36  9708  8t6e48  9719  nn0uz  9781  nnuz  9782  xaddcom  10086  ioomax  10173  iccmax  10174  ioopos  10175  ioorp  10176  fseq1p1m1  10319  fzo0to2pr  10453  fzo0to3tp  10454  frecfzennn  10678  irec  10891  sq10e99m1  10965  facnn  10979  fac0  10980  faclbnd2  10994  zfz1isolemsplit  11092  minmax  11781  xrminmax  11816  fisumrev2  11997  fsumparts  12021  fsumiun  12028  isumnn0nn  12044  fprod2d  12174  fprodle  12191  ege2le3  12222  cos1bnd  12310  efieq1re  12323  eirraplem  12328  3dvds  12415  m1bits  12511  phiprmpw  12784  4sqlem11  12964  4sqlem19  12972  dec5dvds  12975  decsplit1  12991  unennn  13008  ennnfonelemjn  13013  qnnen  13042  strle1g  13179  quslem  13397  rmodislmod  14355  tgrest  14883  uniretop  15239  cnfldtopn  15253  dvexp  15425  dvef  15441  elply2  15449  cospi  15514  sincos6thpi  15556  lgsdir2lem2  15748  lgsquadlem2  15797  lgsquad2lem2  15801  2lgsoddprmlem3c  15828  bj-omind  16465