Theorem eqtr4i 2164

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

Syntax hints:   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  3eqtr2i  2167  3eqtr2ri  2168  3eqtr4i  2171  3eqtr4ri  2172  rabab  2710  cbvralcsf  3067  cbvrexcsf  3068  cbvrabcsf  3070  dfin5  3083  dfdif2  3084  uneqin  3332  unrab  3352  inrab  3353  inrab2  3354  difrab  3355  dfrab3ss  3359  rabun2  3360  difidALT  3437  difdifdirss  3452  dfif3  3492  tpidm  3633  dfint2  3781  iunrab  3868  uniiun  3874  intiin  3875  0iin  3879  mptv  4033  xpundi  4603  xpundir  4604  resiun2  4847  resopab  4871  opabresid  4880  dfse2  4920  cnvun  4952  cnvin  4954  imaundir  4960  imainrect  4992  cnvcnv2  5000  cnvcnvres  5010  dmtpop  5022  rnsnopg  5025  rnco2  5054  dmco  5055  co01  5061  unidmrn  5079  dfdm2  5081  funimaexg  5215  dfmpt3  5253  mptun  5262  funcocnv2  5400  fnasrn  5606  fnasrng  5608  fpr  5610  fmptap  5618  riotav  5743  dmoprab  5860  rnoprab2  5863  mpov  5869  mpomptx  5870  abrexex2g  6026  abrexex2  6030  1stval2  6061  2ndval2  6062  fo1st  6063  fo2nd  6064  xp2  6079  dfoprab4f  6099  fmpoco  6121  tposmpo  6186  recsfval  6220  frecfnom  6306  freccllem  6307  frecfcllem  6309  frecsuclem  6311  df2o3  6335  o1p1e2  6372  ecqs  6499  qliftf  6522  erovlem  6529  mapsnf1o3  6599  ixp0x  6628  xpf1o  6746  djuunr  6959  dmaddpq  7211  dmmulpq  7212  enq0enq  7263  nqprlu  7379  m1p1sr  7592  m1m1sr  7593  caucvgsr  7634  dfcnqs  7673  3m1e2  8864  2p2e4  8871  3p2e5  8885  3p3e6  8886  4p2e6  8887  4p3e7  8888  4p4e8  8889  5p2e7  8890  5p3e8  8891  5p4e9  8892  6p2e8  8893  6p3e9  8894  7p2e9  8895  nn0supp  9053  nnzrab  9102  nn0zrab  9103  dec0u  9226  dec0h  9227  decsuc  9236  decsucc  9246  numma  9249  decma  9256  decmac  9257  decma2c  9258  decadd  9259  decaddc  9260  decmul1  9269  decmul1c  9270  decmul2c  9271  5p5e10  9276  6p4e10  9277  7p3e10  9280  8p2e10  9285  5t5e25  9308  6t6e36  9313  8t6e48  9324  nn0uz  9384  nnuz  9385  xaddcom  9674  ioomax  9761  iccmax  9762  ioopos  9763  ioorp  9764  fseq1p1m1  9905  fzo0to2pr  10026  fzo0to3tp  10027  frecfzennn  10230  irec  10423  sq10e99m1  10491  facnn  10505  fac0  10506  faclbnd2  10520  zfz1isolemsplit  10613  minmax  11033  xrminmax  11066  fisumrev2  11247  fsumparts  11271  fsumiun  11278  isumnn0nn  11294  ege2le3  11414  cos1bnd  11502  efieq1re  11514  eirraplem  11519  phiprmpw  11934  unennn  11946  ennnfonelemjn  11951  qnnen  11980  strle1g  12088  tgrest  12377  uniretop  12733  dvexp  12883  dvef  12896  cospi  12929  sincos6thpi  12971  bj-omind  13303