Theorem eqtr4i 2253

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 2233	. 2 |- B = C
4	1, 3	eqtri 2250	1 |- A = C

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr2i  2256  3eqtr2ri  2257  3eqtr4i  2260  3eqtr4ri  2261  rabab  2821  cbvralcsf  3187  cbvrexcsf  3188  cbvrabcsf  3190  dfin5  3204  dfdif2  3205  uneqin  3455  unrab  3475  inrab  3476  inrab2  3477  difrab  3478  dfrab3ss  3482  rabun2  3483  difidALT  3561  difdifdirss  3576  dfif3  3616  tpidm  3768  dfint2  3925  iunrab  4013  uniiun  4019  intiin  4020  0iin  4024  mptv  4181  xpundi  4775  xpundir  4776  resiun2  5025  resopab  5049  mptresid  5059  dfse2  5101  cnvun  5134  cnvin  5136  imaundir  5142  imainrect  5174  cnvcnv2  5182  cnvcnvres  5192  dmtpop  5204  rnsnopg  5207  rnco2  5236  dmco  5237  co01  5243  unidmrn  5261  dfdm2  5263  funimaexg  5405  dfmpt3  5446  mptun  5455  funcocnv2  5597  fnasrn  5813  fnasrng  5815  fpr  5821  fmptap  5829  riotav  5960  dmoprab  6085  rnoprab2  6088  mpov  6094  mpomptx  6095  abrexex2g  6265  abrexex2  6269  1stval2  6301  2ndval2  6302  fo1st  6303  fo2nd  6304  xp2  6319  dfoprab4f  6339  fmpoco  6362  tposmpo  6427  recsfval  6461  frecfnom  6547  freccllem  6548  frecfcllem  6550  frecsuclem  6552  df2o3  6576  o1p1e2  6614  ecqs  6744  qliftf  6767  erovlem  6774  mapsnf1o3  6844  ixp0x  6873  xpf1o  7005  djuunr  7233  dmaddpq  7566  dmmulpq  7567  enq0enq  7618  nqprlu  7734  m1p1sr  7947  m1m1sr  7948  caucvgsr  7989  dfcnqs  8028  3m1e2  9230  2p2e4  9237  3p2e5  9252  3p3e6  9253  4p2e6  9254  4p3e7  9255  4p4e8  9256  5p2e7  9257  5p3e8  9258  5p4e9  9259  6p2e8  9260  6p3e9  9261  7p2e9  9262  nn0supp  9421  nnzrab  9470  nn0zrab  9471  dec0u  9598  dec0h  9599  decsuc  9608  decsucc  9618  numma  9621  decma  9628  decmac  9629  decma2c  9630  decadd  9631  decaddc  9632  decmul1  9641  decmul1c  9642  decmul2c  9643  5p5e10  9648  6p4e10  9649  7p3e10  9652  8p2e10  9657  5t5e25  9680  6t6e36  9685  8t6e48  9696  nn0uz  9757  nnuz  9758  xaddcom  10057  ioomax  10144  iccmax  10145  ioopos  10146  ioorp  10147  fseq1p1m1  10290  fzo0to2pr  10424  fzo0to3tp  10425  frecfzennn  10648  irec  10861  sq10e99m1  10935  facnn  10949  fac0  10950  faclbnd2  10964  zfz1isolemsplit  11060  minmax  11741  xrminmax  11776  fisumrev2  11957  fsumparts  11981  fsumiun  11988  isumnn0nn  12004  fprod2d  12134  fprodle  12151  ege2le3  12182  cos1bnd  12270  efieq1re  12283  eirraplem  12288  3dvds  12375  m1bits  12471  phiprmpw  12744  4sqlem11  12924  4sqlem19  12932  dec5dvds  12935  decsplit1  12951  unennn  12968  ennnfonelemjn  12973  qnnen  13002  strle1g  13139  quslem  13357  rmodislmod  14315  tgrest  14843  uniretop  15199  cnfldtopn  15213  dvexp  15385  dvef  15401  elply2  15409  cospi  15474  sincos6thpi  15516  lgsdir2lem2  15708  lgsquadlem2  15757  lgsquad2lem2  15761  2lgsoddprmlem3c  15788  bj-omind  16297