Theorem eqtr4i 2230

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

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  3eqtr2i  2233  3eqtr2ri  2234  3eqtr4i  2237  3eqtr4ri  2238  rabab  2795  cbvralcsf  3160  cbvrexcsf  3161  cbvrabcsf  3163  dfin5  3177  dfdif2  3178  uneqin  3428  unrab  3448  inrab  3449  inrab2  3450  difrab  3451  dfrab3ss  3455  rabun2  3456  difidALT  3534  difdifdirss  3549  dfif3  3589  tpidm  3740  dfint2  3893  iunrab  3981  uniiun  3987  intiin  3988  0iin  3992  mptv  4149  xpundi  4739  xpundir  4740  resiun2  4988  resopab  5012  mptresid  5022  dfse2  5064  cnvun  5097  cnvin  5099  imaundir  5105  imainrect  5137  cnvcnv2  5145  cnvcnvres  5155  dmtpop  5167  rnsnopg  5170  rnco2  5199  dmco  5200  co01  5206  unidmrn  5224  dfdm2  5226  funimaexg  5367  dfmpt3  5408  mptun  5417  funcocnv2  5559  fnasrn  5771  fnasrng  5773  fpr  5779  fmptap  5787  riotav  5918  dmoprab  6039  rnoprab2  6042  mpov  6048  mpomptx  6049  abrexex2g  6218  abrexex2  6222  1stval2  6254  2ndval2  6255  fo1st  6256  fo2nd  6257  xp2  6272  dfoprab4f  6292  fmpoco  6315  tposmpo  6380  recsfval  6414  frecfnom  6500  freccllem  6501  frecfcllem  6503  frecsuclem  6505  df2o3  6529  o1p1e2  6567  ecqs  6697  qliftf  6720  erovlem  6727  mapsnf1o3  6797  ixp0x  6826  xpf1o  6956  djuunr  7183  dmaddpq  7512  dmmulpq  7513  enq0enq  7564  nqprlu  7680  m1p1sr  7893  m1m1sr  7894  caucvgsr  7935  dfcnqs  7974  3m1e2  9176  2p2e4  9183  3p2e5  9198  3p3e6  9199  4p2e6  9200  4p3e7  9201  4p4e8  9202  5p2e7  9203  5p3e8  9204  5p4e9  9205  6p2e8  9206  6p3e9  9207  7p2e9  9208  nn0supp  9367  nnzrab  9416  nn0zrab  9417  dec0u  9544  dec0h  9545  decsuc  9554  decsucc  9564  numma  9567  decma  9574  decmac  9575  decma2c  9576  decadd  9577  decaddc  9578  decmul1  9587  decmul1c  9588  decmul2c  9589  5p5e10  9594  6p4e10  9595  7p3e10  9598  8p2e10  9603  5t5e25  9626  6t6e36  9631  8t6e48  9642  nn0uz  9703  nnuz  9704  xaddcom  10003  ioomax  10090  iccmax  10091  ioopos  10092  ioorp  10093  fseq1p1m1  10236  fzo0to2pr  10369  fzo0to3tp  10370  frecfzennn  10593  irec  10806  sq10e99m1  10880  facnn  10894  fac0  10895  faclbnd2  10909  zfz1isolemsplit  11005  minmax  11616  xrminmax  11651  fisumrev2  11832  fsumparts  11856  fsumiun  11863  isumnn0nn  11879  fprod2d  12009  fprodle  12026  ege2le3  12057  cos1bnd  12145  efieq1re  12158  eirraplem  12163  3dvds  12250  m1bits  12346  phiprmpw  12619  4sqlem11  12799  4sqlem19  12807  dec5dvds  12810  decsplit1  12826  unennn  12843  ennnfonelemjn  12848  qnnen  12877  strle1g  13013  quslem  13231  rmodislmod  14188  tgrest  14716  uniretop  15072  cnfldtopn  15086  dvexp  15258  dvef  15274  elply2  15282  cospi  15347  sincos6thpi  15389  lgsdir2lem2  15581  lgsquadlem2  15630  lgsquad2lem2  15634  2lgsoddprmlem3c  15661  bj-omind  16008