Theorem eqtr4i 2262

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr4i.1	|- A = B
eqtr4i.2	|- C = B

Assertion

Ref	Expression
eqtr4i	|- A = C

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 |- A = B
2		eqtr4i.2	. . 3 |- C = B
3	2	eqcomi 2242	. 2 |- B = C
4	1, 3	eqtri 2259	1 |- A = C

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  4230  xpundi  4833  xpundir  4834  resiun2  5085  resopab  5110  mptresid  5120  dfse2  5163  cnvun  5196  cnvin  5198  imaundir  5204  imainrect  5236  cnvcnv2  5244  cnvcnvres  5254  dmtpop  5266  rnsnopg  5269  rnco2  5298  dmco  5299  co01  5305  unidmrn  5323  dfdm2  5325  funimaexg  5468  dfmpt3  5509  mptun  5518  funcocnv2  5667  fnasrn  5890  fnasrng  5892  fpr  5900  fmptap  5908  riotav  6047  dmoprab  6172  rnoprab2  6175  mpov  6181  mpomptx  6182  abrexex2g  6353  abrexex2  6357  1stval2  6393  2ndval2  6394  fo1st  6395  fo2nd  6396  xp2  6411  dfoprab4f  6431  fmpoco  6456  tposmpo  6556  recsfval  6590  frecfnom  6676  freccllem  6677  frecfcllem  6679  frecsuclem  6681  df2o3  6706  o1p1e2  6745  ecqs  6875  qliftf  6898  erovlem  6905  fset0  6953  mapsnf1o3  6983  ixp0x  7012  xpf1o  7148  djuunr  7412  dmaddpq  7752  dmmulpq  7753  enq0enq  7804  nqprlu  7920  m1p1sr  8133  m1m1sr  8134  caucvgsr  8175  dfcnqs  8214  3m1e2  9433  2p2e4  9440  3p2e5  9455  3p3e6  9456  4p2e6  9457  4p3e7  9458  4p4e8  9459  5p2e7  9460  5p3e8  9461  5p4e9  9462  6p2e8  9463  6p3e9  9464  7p2e9  9465  nn0supp  9630  nnzrab  9679  nn0zrab  9680  dec0u  9813  dec0h  9814  decsuc  9823  decsucc  9833  numma  9836  decma  9843  decmac  9844  decma2c  9845  decadd  9846  decaddc  9847  decmul1  9856  decmul1c  9857  decmul2c  9858  5p5e10  9863  6p4e10  9864  7p3e10  9867  8p2e10  9872  5t5e25  9895  6t6e36  9900  8t6e48  9911  nn0uz  9973  nnuz  9974  xaddcom  10280  ioomax  10367  iccmax  10368  ioopos  10369  ioorp  10370  fseq1p1m1  10518  fzo0to2pr  10653  fzo0to3tp  10654  frecfzennn  10884  irec  11097  sq10e99m1  11173  facnn  11187  fac0  11188  faclbnd2  11202  hashf1lem2  11308  zfz1isolemsplit  11312  minmax  12020  xrminmax  12056  fisumrev2  12238  fsumparts  12262  fsumiun  12269  isumnn0nn  12285  fprod2d  12415  fprodle  12432  ege2le3  12463  cos1bnd  12551  efieq1re  12564  eirraplem  12569  3dvds  12656  m1bits  12752  phiprmpw  13029  4sqlem11  13209  4sqlem19  13217  dec5dvds  13220  decsplit1  13237  5prm  13252  7prm  13254  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilemfval  13287  ballotfilemth  13339  unennn  13346  ennnfonelemjn  13351  qnnen  13380  strle1g  13519  quslem  13704  elcntr  14163  cntri  14165  cntrsubgnsg  14175  cntrnsg  14176  gsump1  14247  gsum2dfilem2  14272  rmodislmod  14797  tgrest  15395  uniretop  15751  cnfldtopn  15765  dvexp  15937  dvef  15953  elply2  15961  cospi  16027  sincos6thpi  16069  logfac  16126  log2ublem3  16223  birthdaylog2  16228  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  ppi2  16274  ppi3  16275  ppiqub  16293  chtqub  16296  bclbnd  16307  bposlem8  16318  lgsdir2lem2  16353  lgsquadlem2  16402  lgsquad2lem2  16406  2lgsoddprmlem3c  16433  konigsbergumgr  16933  konigsberglem1  16934  konigsberglem2  16935  bj-omind  17165