Theorem eqtr4i 2217

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

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr2i  2220  3eqtr2ri  2221  3eqtr4i  2224  3eqtr4ri  2225  rabab  2781  cbvralcsf  3144  cbvrexcsf  3145  cbvrabcsf  3147  dfin5  3161  dfdif2  3162  uneqin  3411  unrab  3431  inrab  3432  inrab2  3433  difrab  3434  dfrab3ss  3438  rabun2  3439  difidALT  3517  difdifdirss  3532  dfif3  3571  tpidm  3721  dfint2  3873  iunrab  3961  uniiun  3967  intiin  3968  0iin  3972  mptv  4127  xpundi  4716  xpundir  4717  resiun2  4963  resopab  4987  mptresid  4997  dfse2  5039  cnvun  5072  cnvin  5074  imaundir  5080  imainrect  5112  cnvcnv2  5120  cnvcnvres  5130  dmtpop  5142  rnsnopg  5145  rnco2  5174  dmco  5175  co01  5181  unidmrn  5199  dfdm2  5201  funimaexg  5339  dfmpt3  5377  mptun  5386  funcocnv2  5526  fnasrn  5737  fnasrng  5739  fpr  5741  fmptap  5749  riotav  5880  dmoprab  6000  rnoprab2  6003  mpov  6009  mpomptx  6010  abrexex2g  6174  abrexex2  6178  1stval2  6210  2ndval2  6211  fo1st  6212  fo2nd  6213  xp2  6228  dfoprab4f  6248  fmpoco  6271  tposmpo  6336  recsfval  6370  frecfnom  6456  freccllem  6457  frecfcllem  6459  frecsuclem  6461  df2o3  6485  o1p1e2  6523  ecqs  6653  qliftf  6676  erovlem  6683  mapsnf1o3  6753  ixp0x  6782  xpf1o  6902  djuunr  7127  dmaddpq  7441  dmmulpq  7442  enq0enq  7493  nqprlu  7609  m1p1sr  7822  m1m1sr  7823  caucvgsr  7864  dfcnqs  7903  3m1e2  9104  2p2e4  9111  3p2e5  9126  3p3e6  9127  4p2e6  9128  4p3e7  9129  4p4e8  9130  5p2e7  9131  5p3e8  9132  5p4e9  9133  6p2e8  9134  6p3e9  9135  7p2e9  9136  nn0supp  9295  nnzrab  9344  nn0zrab  9345  dec0u  9471  dec0h  9472  decsuc  9481  decsucc  9491  numma  9494  decma  9501  decmac  9502  decma2c  9503  decadd  9504  decaddc  9505  decmul1  9514  decmul1c  9515  decmul2c  9516  5p5e10  9521  6p4e10  9522  7p3e10  9525  8p2e10  9530  5t5e25  9553  6t6e36  9558  8t6e48  9569  nn0uz  9630  nnuz  9631  xaddcom  9930  ioomax  10017  iccmax  10018  ioopos  10019  ioorp  10020  fseq1p1m1  10163  fzo0to2pr  10288  fzo0to3tp  10289  frecfzennn  10500  irec  10713  sq10e99m1  10787  facnn  10801  fac0  10802  faclbnd2  10816  zfz1isolemsplit  10912  minmax  11376  xrminmax  11411  fisumrev2  11592  fsumparts  11616  fsumiun  11623  isumnn0nn  11639  fprod2d  11769  fprodle  11786  ege2le3  11817  cos1bnd  11905  efieq1re  11918  eirraplem  11923  phiprmpw  12363  4sqlem11  12542  4sqlem19  12550  unennn  12557  ennnfonelemjn  12562  qnnen  12591  strle1g  12727  quslem  12910  rmodislmod  13850  tgrest  14348  uniretop  14704  cnfldtopn  14718  dvexp  14890  dvef  14906  elply2  14914  cospi  14976  sincos6thpi  15018  lgsdir2lem2  15186  lgsquadlem2  15235  lgsquad2lem2  15239  2lgsoddprmlem3c  15266  bj-omind  15496