Theorem eqtr4i 2220

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr2i  2223  3eqtr2ri  2224  3eqtr4i  2227  3eqtr4ri  2228  rabab  2784  cbvralcsf  3147  cbvrexcsf  3148  cbvrabcsf  3150  dfin5  3164  dfdif2  3165  uneqin  3415  unrab  3435  inrab  3436  inrab2  3437  difrab  3438  dfrab3ss  3442  rabun2  3443  difidALT  3521  difdifdirss  3536  dfif3  3575  tpidm  3725  dfint2  3877  iunrab  3965  uniiun  3971  intiin  3972  0iin  3976  mptv  4131  xpundi  4720  xpundir  4721  resiun2  4967  resopab  4991  mptresid  5001  dfse2  5043  cnvun  5076  cnvin  5078  imaundir  5084  imainrect  5116  cnvcnv2  5124  cnvcnvres  5134  dmtpop  5146  rnsnopg  5149  rnco2  5178  dmco  5179  co01  5185  unidmrn  5203  dfdm2  5205  funimaexg  5343  dfmpt3  5383  mptun  5392  funcocnv2  5532  fnasrn  5743  fnasrng  5745  fpr  5747  fmptap  5755  riotav  5886  dmoprab  6007  rnoprab2  6010  mpov  6016  mpomptx  6017  abrexex2g  6186  abrexex2  6190  1stval2  6222  2ndval2  6223  fo1st  6224  fo2nd  6225  xp2  6240  dfoprab4f  6260  fmpoco  6283  tposmpo  6348  recsfval  6382  frecfnom  6468  freccllem  6469  frecfcllem  6471  frecsuclem  6473  df2o3  6497  o1p1e2  6535  ecqs  6665  qliftf  6688  erovlem  6695  mapsnf1o3  6765  ixp0x  6794  xpf1o  6914  djuunr  7141  dmaddpq  7463  dmmulpq  7464  enq0enq  7515  nqprlu  7631  m1p1sr  7844  m1m1sr  7845  caucvgsr  7886  dfcnqs  7925  3m1e2  9127  2p2e4  9134  3p2e5  9149  3p3e6  9150  4p2e6  9151  4p3e7  9152  4p4e8  9153  5p2e7  9154  5p3e8  9155  5p4e9  9156  6p2e8  9157  6p3e9  9158  7p2e9  9159  nn0supp  9318  nnzrab  9367  nn0zrab  9368  dec0u  9494  dec0h  9495  decsuc  9504  decsucc  9514  numma  9517  decma  9524  decmac  9525  decma2c  9526  decadd  9527  decaddc  9528  decmul1  9537  decmul1c  9538  decmul2c  9539  5p5e10  9544  6p4e10  9545  7p3e10  9548  8p2e10  9553  5t5e25  9576  6t6e36  9581  8t6e48  9592  nn0uz  9653  nnuz  9654  xaddcom  9953  ioomax  10040  iccmax  10041  ioopos  10042  ioorp  10043  fseq1p1m1  10186  fzo0to2pr  10311  fzo0to3tp  10312  frecfzennn  10535  irec  10748  sq10e99m1  10822  facnn  10836  fac0  10837  faclbnd2  10851  zfz1isolemsplit  10947  minmax  11412  xrminmax  11447  fisumrev2  11628  fsumparts  11652  fsumiun  11659  isumnn0nn  11675  fprod2d  11805  fprodle  11822  ege2le3  11853  cos1bnd  11941  efieq1re  11954  eirraplem  11959  3dvds  12046  m1bits  12142  phiprmpw  12415  4sqlem11  12595  4sqlem19  12603  dec5dvds  12606  decsplit1  12622  unennn  12639  ennnfonelemjn  12644  qnnen  12673  strle1g  12809  quslem  13026  rmodislmod  13983  tgrest  14489  uniretop  14845  cnfldtopn  14859  dvexp  15031  dvef  15047  elply2  15055  cospi  15120  sincos6thpi  15162  lgsdir2lem2  15354  lgsquadlem2  15403  lgsquad2lem2  15407  2lgsoddprmlem3c  15434  bj-omind  15664