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  2834  cbvralcsf  3200  cbvrexcsf  3201  cbvrabcsf  3203  dfin5  3217  dfdif2  3218  uneqin  3471  unrab  3491  inrab  3492  inrab2  3493  difrab  3494  dfrab3ss  3498  rabun2  3499  difidALT  3577  difdifdirss  3593  dfif3  3635  tpidm  3792  dfint2  3950  iunrab  4038  uniiun  4044  intiin  4045  0iin  4049  mptv  4206  xpundi  4805  xpundir  4806  resiun2  5057  resopab  5081  mptresid  5091  dfse2  5134  cnvun  5167  cnvin  5169  imaundir  5175  imainrect  5207  cnvcnv2  5215  cnvcnvres  5225  dmtpop  5237  rnsnopg  5240  rnco2  5269  dmco  5270  co01  5276  unidmrn  5294  dfdm2  5296  funimaexg  5439  dfmpt3  5480  mptun  5489  funcocnv2  5638  fnasrn  5855  fnasrng  5857  fpr  5865  fmptap  5873  riotav  6008  dmoprab  6133  rnoprab2  6136  mpov  6142  mpomptx  6143  abrexex2g  6312  abrexex2  6316  1stval2  6348  2ndval2  6349  fo1st  6350  fo2nd  6351  xp2  6366  dfoprab4f  6386  fmpoco  6411  tposmpo  6511  recsfval  6545  frecfnom  6631  freccllem  6632  frecfcllem  6634  frecsuclem  6636  df2o3  6661  o1p1e2  6700  ecqs  6830  qliftf  6853  erovlem  6860  mapsnf1o3  6931  ixp0x  6960  xpf1o  7096  djuunr  7356  dmaddpq  7693  dmmulpq  7694  enq0enq  7745  nqprlu  7861  m1p1sr  8074  m1m1sr  8075  caucvgsr  8116  dfcnqs  8155  3m1e2  9356  2p2e4  9363  3p2e5  9378  3p3e6  9379  4p2e6  9380  4p3e7  9381  4p4e8  9382  5p2e7  9383  5p3e8  9384  5p4e9  9385  6p2e8  9386  6p3e9  9387  7p2e9  9388  nn0supp  9551  nnzrab  9600  nn0zrab  9601  dec0u  9728  dec0h  9729  decsuc  9738  decsucc  9748  numma  9751  decma  9758  decmac  9759  decma2c  9760  decadd  9761  decaddc  9762  decmul1  9771  decmul1c  9772  decmul2c  9773  5p5e10  9778  6p4e10  9779  7p3e10  9782  8p2e10  9787  5t5e25  9810  6t6e36  9815  8t6e48  9826  nn0uz  9888  nnuz  9889  xaddcom  10193  ioomax  10280  iccmax  10281  ioopos  10282  ioorp  10283  fseq1p1m1  10427  fzo0to2pr  10562  fzo0to3tp  10563  frecfzennn  10787  irec  11000  sq10e99m1  11074  facnn  11088  fac0  11089  faclbnd2  11103  zfz1isolemsplit  11206  minmax  11911  xrminmax  11946  fisumrev2  12128  fsumparts  12152  fsumiun  12159  isumnn0nn  12175  fprod2d  12305  fprodle  12322  ege2le3  12353  cos1bnd  12441  efieq1re  12454  eirraplem  12459  3dvds  12546  m1bits  12642  phiprmpw  12915  4sqlem11  13095  4sqlem19  13103  dec5dvds  13106  decsplit1  13122  unennn  13140  ennnfonelemjn  13145  qnnen  13174  strle1g  13311  quslem  13529  rmodislmod  14491  tgrest  15026  uniretop  15382  cnfldtopn  15396  dvexp  15568  dvef  15584  elply2  15592  cospi  15657  sincos6thpi  15699  lgsdir2lem2  15894  lgsquadlem2  15943  lgsquad2lem2  15947  2lgsoddprmlem3c  15974  konigsbergumgr  16474  konigsberglem1  16475  konigsberglem2  16476  bj-omind  16696  gfsump1  16859