Theorem eqtr4i 2104

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

Syntax hints:   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  3eqtr2i  2107  3eqtr2ri  2108  3eqtr4i  2111  3eqtr4ri  2112  rabab  2620  cbvralcsf  2964  cbvrexcsf  2965  cbvrabcsf  2967  dfin5  2980  dfdif2  2981  uneqin  3215  unrab  3235  inrab  3236  inrab2  3237  difrab  3238  dfrab3ss  3242  rabun2  3243  difidALT  3313  difdifdirss  3327  dfif3  3364  tpidm  3494  dfint2  3638  iunrab  3725  uniiun  3731  intiin  3732  0iin  3736  mptv  3874  xpundi  4414  xpundir  4415  resiun2  4649  resopab  4672  opabresid  4679  dfse2  4718  cnvun  4749  cnvin  4751  imaundir  4757  imainrect  4786  cnvcnv2  4794  cnvcnvres  4804  dmtpop  4816  rnsnopg  4819  rnco2  4848  dmco  4849  co01  4855  unidmrn  4870  dfdm2  4872  funimaexg  5003  dfmpt3  5041  mptun  5049  funcocnv2  5171  fnasrn  5362  fnasrng  5364  fpr  5366  fmptap  5374  riotav  5493  dmoprab  5605  rnoprab2  5608  mpt2v  5614  mpt2mptx  5615  abrexex2g  5767  abrexex2  5771  1stval2  5802  2ndval2  5803  fo1st  5804  fo2nd  5805  xp2  5819  dfoprab4f  5839  fmpt2co  5857  tposmpt2  5919  recsfval  5954  frecfnom  6009  frecsuclem1  6010  frecsuclem2  6012  df2o3  6037  o1p1e2  6071  ecqs  6191  qliftf  6214  erovlem  6221  dmaddpq  6569  dmmulpq  6570  enq0enq  6621  nqprlu  6737  m1p1sr  6937  m1m1sr  6938  caucvgsr  6978  dfcnqs  7009  3m1e2  8158  2p2e4  8159  3p2e5  8173  3p3e6  8174  4p2e6  8175  4p3e7  8176  4p4e8  8177  5p2e7  8178  5p3e8  8179  5p4e9  8180  6p2e8  8181  6p3e9  8182  7p2e9  8183  nn0supp  8340  nnzrab  8375  nn0zrab  8376  dec0u  8497  dec0h  8498  decsuc  8507  decsucc  8517  numma  8520  decma  8527  decmac  8528  decma2c  8529  decadd  8530  decaddc  8531  decmul1  8540  decmul1c  8541  decmul2c  8542  5p5e10  8547  6p4e10  8548  7p3e10  8551  8p2e10  8556  5t5e25  8579  6t6e36  8584  8t6e48  8595  nn0uz  8653  nnuz  8654  ioomax  8971  iccmax  8972  ioopos  8973  ioorp  8974  fseq1p1m1  9111  fzo0to2pr  9227  fzo0to3tp  9228  frecfzennn  9419  irec  9574  sq10e99m1  9641  facnn  9654  fac0  9655  faclbnd2  9669  minmax  10112  bj-omind  10729