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

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced 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  3812  dfint2  3970  iunrab  4058  uniiun  4064  intiin  4065  0iin  4069  mptv  4226  xpundi  4829  xpundir  4830  resiun2  5081  resopab  5105  mptresid  5115  dfse2  5158  cnvun  5191  cnvin  5193  imaundir  5199  imainrect  5231  cnvcnv2  5239  cnvcnvres  5249  dmtpop  5261  rnsnopg  5264  rnco2  5293  dmco  5294  co01  5300  unidmrn  5318  dfdm2  5320  funimaexg  5463  dfmpt3  5504  mptun  5513  funcocnv2  5662  fnasrn  5881  fnasrng  5883  fpr  5891  fmptap  5899  riotav  6037  dmoprab  6162  rnoprab2  6165  mpov  6171  mpomptx  6172  abrexex2g  6342  abrexex2  6346  1stval2  6382  2ndval2  6383  fo1st  6384  fo2nd  6385  xp2  6400  dfoprab4f  6420  fmpoco  6445  tposmpo  6545  recsfval  6579  frecfnom  6665  freccllem  6666  frecfcllem  6668  frecsuclem  6670  df2o3  6695  o1p1e2  6734  ecqs  6864  qliftf  6887  erovlem  6894  fset0  6942  mapsnf1o3  6972  ixp0x  7001  xpf1o  7137  djuunr  7399  dmaddpq  7739  dmmulpq  7740  enq0enq  7791  nqprlu  7907  m1p1sr  8120  m1m1sr  8121  caucvgsr  8162  dfcnqs  8201  3m1e2  9406  2p2e4  9413  3p2e5  9428  3p3e6  9429  4p2e6  9430  4p3e7  9431  4p4e8  9432  5p2e7  9433  5p3e8  9434  5p4e9  9435  6p2e8  9436  6p3e9  9437  7p2e9  9438  nn0supp  9601  nnzrab  9650  nn0zrab  9651  dec0u  9779  dec0h  9780  decsuc  9789  decsucc  9799  numma  9802  decma  9809  decmac  9810  decma2c  9811  decadd  9812  decaddc  9813  decmul1  9822  decmul1c  9823  decmul2c  9824  5p5e10  9829  6p4e10  9830  7p3e10  9833  8p2e10  9838  5t5e25  9861  6t6e36  9866  8t6e48  9877  nn0uz  9939  nnuz  9940  xaddcom  10245  ioomax  10332  iccmax  10333  ioopos  10334  ioorp  10335  fseq1p1m1  10482  fzo0to2pr  10617  fzo0to3tp  10618  frecfzennn  10844  irec  11057  sq10e99m1  11132  facnn  11146  fac0  11147  faclbnd2  11161  hashf1lem2  11267  zfz1isolemsplit  11271  minmax  11977  xrminmax  12012  fisumrev2  12194  fsumparts  12218  fsumiun  12225  isumnn0nn  12241  fprod2d  12371  fprodle  12388  ege2le3  12419  cos1bnd  12507  efieq1re  12520  eirraplem  12525  3dvds  12612  m1bits  12708  phiprmpw  12981  4sqlem11  13161  4sqlem19  13169  dec5dvds  13172  decsplit1  13188  ballotfilemfval  13210  ballotfilemth  13262  unennn  13269  ennnfonelemjn  13274  qnnen  13303  strle1g  13440  quslem  13625  gsump1  14137  rmodislmod  14663  tgrest  15196  uniretop  15552  cnfldtopn  15566  dvexp  15738  dvef  15754  elply2  15762  cospi  15827  sincos6thpi  15869  logfac  15921  lgsdir2lem2  16065  lgsquadlem2  16114  lgsquad2lem2  16118  2lgsoddprmlem3c  16145  konigsbergumgr  16645  konigsberglem1  16646  konigsberglem2  16647  bj-omind  16877