Theorem eqtr4i 2255

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtr2i  2258  3eqtr2ri  2259  3eqtr4i  2262  3eqtr4ri  2263  rabab  2825  cbvralcsf  3191  cbvrexcsf  3192  cbvrabcsf  3194  dfin5  3208  dfdif2  3209  uneqin  3460  unrab  3480  inrab  3481  inrab2  3482  difrab  3483  dfrab3ss  3487  rabun2  3488  difidALT  3566  difdifdirss  3581  dfif3  3623  tpidm  3777  dfint2  3935  iunrab  4023  uniiun  4029  intiin  4030  0iin  4034  mptv  4191  xpundi  4788  xpundir  4789  resiun2  5039  resopab  5063  mptresid  5073  dfse2  5116  cnvun  5149  cnvin  5151  imaundir  5157  imainrect  5189  cnvcnv2  5197  cnvcnvres  5207  dmtpop  5219  rnsnopg  5222  rnco2  5251  dmco  5252  co01  5258  unidmrn  5276  dfdm2  5278  funimaexg  5421  dfmpt3  5462  mptun  5471  funcocnv2  5617  fnasrn  5834  fnasrng  5836  fpr  5844  fmptap  5852  riotav  5987  dmoprab  6112  rnoprab2  6115  mpov  6121  mpomptx  6122  abrexex2g  6291  abrexex2  6295  1stval2  6327  2ndval2  6328  fo1st  6329  fo2nd  6330  xp2  6345  dfoprab4f  6365  fmpoco  6390  tposmpo  6490  recsfval  6524  frecfnom  6610  freccllem  6611  frecfcllem  6613  frecsuclem  6615  df2o3  6640  o1p1e2  6679  ecqs  6809  qliftf  6832  erovlem  6839  mapsnf1o3  6909  ixp0x  6938  xpf1o  7073  djuunr  7325  dmaddpq  7659  dmmulpq  7660  enq0enq  7711  nqprlu  7827  m1p1sr  8040  m1m1sr  8041  caucvgsr  8082  dfcnqs  8121  3m1e2  9322  2p2e4  9329  3p2e5  9344  3p3e6  9345  4p2e6  9346  4p3e7  9347  4p4e8  9348  5p2e7  9349  5p3e8  9350  5p4e9  9351  6p2e8  9352  6p3e9  9353  7p2e9  9354  nn0supp  9515  nnzrab  9564  nn0zrab  9565  dec0u  9692  dec0h  9693  decsuc  9702  decsucc  9712  numma  9715  decma  9722  decmac  9723  decma2c  9724  decadd  9725  decaddc  9726  decmul1  9735  decmul1c  9736  decmul2c  9737  5p5e10  9742  6p4e10  9743  7p3e10  9746  8p2e10  9751  5t5e25  9774  6t6e36  9779  8t6e48  9790  nn0uz  9852  nnuz  9853  xaddcom  10157  ioomax  10244  iccmax  10245  ioopos  10246  ioorp  10247  fseq1p1m1  10391  fzo0to2pr  10526  fzo0to3tp  10527  frecfzennn  10751  irec  10964  sq10e99m1  11038  facnn  11052  fac0  11053  faclbnd2  11067  zfz1isolemsplit  11165  minmax  11870  xrminmax  11905  fisumrev2  12087  fsumparts  12111  fsumiun  12118  isumnn0nn  12134  fprod2d  12264  fprodle  12281  ege2le3  12312  cos1bnd  12400  efieq1re  12413  eirraplem  12418  3dvds  12505  m1bits  12601  phiprmpw  12874  4sqlem11  13054  4sqlem19  13062  dec5dvds  13065  decsplit1  13081  unennn  13098  ennnfonelemjn  13103  qnnen  13132  strle1g  13269  quslem  13487  rmodislmod  14447  tgrest  14980  uniretop  15336  cnfldtopn  15350  dvexp  15522  dvef  15538  elply2  15546  cospi  15611  sincos6thpi  15653  lgsdir2lem2  15848  lgsquadlem2  15897  lgsquad2lem2  15901  2lgsoddprmlem3c  15928  konigsbergumgr  16428  konigsberglem1  16429  konigsberglem2  16430  bj-omind  16650  gfsump1  16815