Theorem eqtr4i 2262

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr2i  2265  3eqtr2ri  2266  3eqtr4i  2269  3eqtr4ri  2270  rabab  2843  cbvralcsf  3210  cbvrexcsf  3211  cbvrabcsf  3213  dfin5  3227  dfdif2  3228  uneqin  3482  unrab  3504  inrab  3505  inrab2  3506  difrab  3507  dfrab3ss  3511  rabun2  3512  dfnul2  3523  difidALT  3595  difdifdirss  3612  dfif3  3654  tpidm  3813  dfint2  3972  iunrab  4060  uniiun  4066  intiin  4067  0iin  4071  mptv  4228  xpundi  4831  xpundir  4832  resiun2  5083  resopab  5107  mptresid  5117  dfse2  5160  cnvun  5193  cnvin  5195  imaundir  5201  imainrect  5233  cnvcnv2  5241  cnvcnvres  5251  dmtpop  5263  rnsnopg  5266  rnco2  5295  dmco  5296  co01  5302  unidmrn  5320  dfdm2  5322  funimaexg  5465  dfmpt3  5506  mptun  5515  funcocnv2  5664  fnasrn  5887  fnasrng  5889  fpr  5897  fmptap  5905  riotav  6044  dmoprab  6169  rnoprab2  6172  mpov  6178  mpomptx  6179  abrexex2g  6349  abrexex2  6353  1stval2  6389  2ndval2  6390  fo1st  6391  fo2nd  6392  xp2  6407  dfoprab4f  6427  fmpoco  6452  tposmpo  6552  recsfval  6586  frecfnom  6672  freccllem  6673  frecfcllem  6675  frecsuclem  6677  df2o3  6702  o1p1e2  6741  ecqs  6871  qliftf  6894  erovlem  6901  fset0  6949  mapsnf1o3  6979  ixp0x  7008  xpf1o  7144  djuunr  7406  dmaddpq  7746  dmmulpq  7747  enq0enq  7798  nqprlu  7914  m1p1sr  8127  m1m1sr  8128  caucvgsr  8169  dfcnqs  8208  3m1e2  9424  2p2e4  9431  3p2e5  9446  3p3e6  9447  4p2e6  9448  4p3e7  9449  4p4e8  9450  5p2e7  9451  5p3e8  9452  5p4e9  9453  6p2e8  9454  6p3e9  9455  7p2e9  9456  nn0supp  9619  nnzrab  9668  nn0zrab  9669  dec0u  9797  dec0h  9798  decsuc  9807  decsucc  9817  numma  9820  decma  9827  decmac  9828  decma2c  9829  decadd  9830  decaddc  9831  decmul1  9840  decmul1c  9841  decmul2c  9842  5p5e10  9847  6p4e10  9848  7p3e10  9851  8p2e10  9856  5t5e25  9879  6t6e36  9884  8t6e48  9895  nn0uz  9957  nnuz  9958  xaddcom  10263  ioomax  10350  iccmax  10351  ioopos  10352  ioorp  10353  fseq1p1m1  10501  fzo0to2pr  10636  fzo0to3tp  10637  frecfzennn  10863  irec  11076  sq10e99m1  11151  facnn  11165  fac0  11166  faclbnd2  11180  hashf1lem2  11286  zfz1isolemsplit  11290  minmax  11996  xrminmax  12031  fisumrev2  12213  fsumparts  12237  fsumiun  12244  isumnn0nn  12260  fprod2d  12390  fprodle  12407  ege2le3  12438  cos1bnd  12526  efieq1re  12539  eirraplem  12544  3dvds  12631  m1bits  12727  phiprmpw  13000  4sqlem11  13180  4sqlem19  13188  dec5dvds  13191  decsplit1  13207  ballotfilemfval  13229  ballotfilemth  13281  unennn  13288  ennnfonelemjn  13293  qnnen  13322  strle1g  13460  quslem  13645  gsump1  14157  rmodislmod  14688  tgrest  15270  uniretop  15626  cnfldtopn  15640  dvexp  15812  dvef  15828  elply2  15836  cospi  15901  sincos6thpi  15943  logfac  15995  log2ublem3  16085  birthdaylog2  16090  lgsdir2lem2  16148  lgsquadlem2  16197  lgsquad2lem2  16201  2lgsoddprmlem3c  16228  konigsbergumgr  16728  konigsberglem1  16729  konigsberglem2  16730  bj-omind  16960