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  6557  recsfval  6591  frecfnom  6677  freccllem  6678  frecfcllem  6680  frecsuclem  6682  df2o3  6707  o1p1e2  6746  ecqs  6876  qliftf  6899  erovlem  6906  fset0  6954  mapsnf1o3  6985  ixp0x  7014  xpf1o  7150  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  9628  nnzrab  9677  nn0zrab  9678  dec0u  9812  dec0h  9813  decsuc  9822  decsucc  9832  numma  9835  decma  9842  decmac  9843  decma2c  9844  decadd  9845  decaddc  9846  decmul1  9855  decmul1c  9856  decmul2c  9857  5p5e10  9862  6p4e10  9863  7p3e10  9866  8p2e10  9871  5t5e25  9894  6t6e36  9899  8t6e48  9910  nn0uz  9972  nnuz  9973  xaddcom  10279  ioomax  10366  iccmax  10367  ioopos  10368  ioorp  10369  fseq1p1m1  10517  fzo0to2pr  10652  fzo0to3tp  10653  frecfzennn  10883  irec  11096  sq10e99m1  11172  facnn  11186  fac0  11187  faclbnd2  11201  hashf1lem2  11307  zfz1isolemsplit  11311  minmax  12019  xrminmax  12055  fisumrev2  12237  fsumparts  12261  fsumiun  12268  isumnn0nn  12284  fprod2d  12414  fprodle  12431  ege2le3  12462  cos1bnd  12550  efieq1re  12563  eirraplem  12568  3dvds  12655  m1bits  12751  phiprmpw  13028  4sqlem11  13208  4sqlem19  13216  dec5dvds  13219  decsplit1  13236  5prm  13251  7prm  13253  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  ballotfilemfval  13286  ballotfilemth  13338  unennn  13345  ennnfonelemjn  13350  qnnen  13379  strle1g  13518  quslem  13703  elcntr  14162  cntri  14164  cntrsubgnsg  14174  cntrnsg  14175  gsump1  14246  gsum2dfilem2  14271  rmodislmod  14796  tgrest  15412  uniretop  15768  cnfldtopn  15782  dvexp  15954  dvef  15970  elply2  15978  cospi  16044  sincos6thpi  16086  logfac  16143  log2ublem3  16240  birthdaylog2  16245  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  ppi2  16291  ppi3  16292  ppiqub  16310  chtqub  16313  bclbnd  16324  bposlem8  16335  lgsdir2lem2  16370  lgsquadlem2  16419  lgsquad2lem2  16423  2lgsoddprmlem3c  16450  konigsbergumgr  16950  konigsberglem1  16951  konigsberglem2  16952  bj-omind  17182