Theorem eqtr4i 2060

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

Syntax hints:   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  3eqtr2i  2063  3eqtr2ri  2064  3eqtr4i  2067  3eqtr4ri  2068  rabab  2569  cbvralcsf  2902  cbvrexcsf  2903  cbvrabcsf  2905  dfin5  2919  dfdif2  2920  uneqin  3182  unrab  3202  inrab  3203  inrab2  3204  difrab  3205  dfrab3ss  3209  rabun2  3210  difidALT  3287  difdifdirss  3301  dfif3  3337  tpidm  3463  dfint2  3608  iunrab  3695  uniiun  3701  intiin  3702  0iin  3706  mptv  3844  xpundi  4339  xpundir  4340  resiun2  4574  resopab  4595  opabresid  4602  dfse2  4641  cnvun  4672  cnvin  4674  imaundir  4680  imainrect  4709  cnvcnv2  4717  cnvcnvres  4727  dmtpop  4739  rnsnopg  4742  rnco2  4771  dmco  4772  co01  4778  unidmrn  4793  dfdm2  4795  funimaexg  4926  dfmpt3  4964  mptun  4972  funcocnv2  5094  fnasrn  5284  fnasrng  5286  fpr  5288  fmptap  5296  riotav  5416  dmoprab  5527  rnoprab2  5530  mpt2v  5536  mpt2mptx  5537  abrexex2g  5689  abrexex2  5693  1stval2  5724  2ndval2  5725  fo1st  5726  fo2nd  5727  xp2  5741  dfoprab4f  5761  fmpt2co  5779  tposmpt2  5837  recsfval  5872  frecfnom  5925  frecsuclem1  5926  frecsuclem2  5928  df2o3  5953  o1p1e2  5987  ecqs  6104  qliftf  6127  erovlem  6134  dmaddpq  6363  dmmulpq  6364  enq0enq  6414  m1p1sr  6688  m1m1sr  6689  dfcnqs  6738  3m1e2  7814  2p2e4  7815  3p2e5  7830  3p3e6  7831  4p2e6  7832  4p3e7  7833  4p4e8  7834  5p2e7  7835  5p3e8  7836  5p4e9  7837  5p5e10  7838  6p2e8  7839  6p3e9  7840  6p4e10  7841  7p2e9  7842  7p3e10  7843  8p2e10  7844  nn0supp  8010  nnzrab  8045  nn0zrab  8046  dec0u  8158  dec0h  8159  decsuc  8166  decsucc  8170  numma  8174  decma  8181  decmac  8182  decma2c  8183  decadd  8184  decaddc  8185  decmul1c  8190  decmul2c  8191  5t5e25  8219  6t6e36  8224  8t6e48  8235  nn0uz  8283  nnuz  8284  ioomax  8587  iccmax  8588  ioopos  8589  ioorp  8590  fseq1p1m1  8726  fzo0to2pr  8844  fzo0to3tp  8845  frecfzennn  8884  irec  9005  bj-omind  9393