Theorem eqtr4i 2262

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr4i.1	⊢ 𝐴 = 𝐵
eqtr4i.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eqtr4i	⊢ 𝐴 = 𝐶

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtr4i.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2242	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2259	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  3eqtr2i  2265  3eqtr2ri  2266  3eqtr4i  2269  3eqtr4ri  2270  rabab  2843  cbvralcsf  3210  cbvrexcsf  3211  cbvrabcsf  3213  dfin5  3227  dfdif2  3228  uneqin  3482  unrab  3504  inrab  3505  inrab2  3506  difrab  3507  dfrab3ss  3511  rabun2  3512  dfnul2  3523  difidALT  3593  difdifdirss  3609  dfif3  3651  tpidm  3809  dfint2  3967  iunrab  4055  uniiun  4061  intiin  4062  0iin  4066  mptv  4223  xpundi  4826  xpundir  4827  resiun2  5078  resopab  5102  mptresid  5112  dfse2  5155  cnvun  5188  cnvin  5190  imaundir  5196  imainrect  5228  cnvcnv2  5236  cnvcnvres  5246  dmtpop  5258  rnsnopg  5261  rnco2  5290  dmco  5291  co01  5297  unidmrn  5315  dfdm2  5317  funimaexg  5460  dfmpt3  5501  mptun  5510  funcocnv2  5659  fnasrn  5878  fnasrng  5880  fpr  5888  fmptap  5896  riotav  6034  dmoprab  6159  rnoprab2  6162  mpov  6168  mpomptx  6169  abrexex2g  6339  abrexex2  6343  1stval2  6379  2ndval2  6380  fo1st  6381  fo2nd  6382  xp2  6397  dfoprab4f  6417  fmpoco  6442  tposmpo  6542  recsfval  6576  frecfnom  6662  freccllem  6663  frecfcllem  6665  frecsuclem  6667  df2o3  6692  o1p1e2  6731  ecqs  6861  qliftf  6884  erovlem  6891  fset0  6939  mapsnf1o3  6969  ixp0x  6998  xpf1o  7134  djuunr  7396  dmaddpq  7736  dmmulpq  7737  enq0enq  7788  nqprlu  7904  m1p1sr  8117  m1m1sr  8118  caucvgsr  8159  dfcnqs  8198  3m1e2  9403  2p2e4  9410  3p2e5  9425  3p3e6  9426  4p2e6  9427  4p3e7  9428  4p4e8  9429  5p2e7  9430  5p3e8  9431  5p4e9  9432  6p2e8  9433  6p3e9  9434  7p2e9  9435  nn0supp  9598  nnzrab  9647  nn0zrab  9648  dec0u  9776  dec0h  9777  decsuc  9786  decsucc  9796  numma  9799  decma  9806  decmac  9807  decma2c  9808  decadd  9809  decaddc  9810  decmul1  9819  decmul1c  9820  decmul2c  9821  5p5e10  9826  6p4e10  9827  7p3e10  9830  8p2e10  9835  5t5e25  9858  6t6e36  9863  8t6e48  9874  nn0uz  9936  nnuz  9937  xaddcom  10242  ioomax  10329  iccmax  10330  ioopos  10331  ioorp  10332  fseq1p1m1  10479  fzo0to2pr  10614  fzo0to3tp  10615  frecfzennn  10841  irec  11054  sq10e99m1  11129  facnn  11143  fac0  11144  faclbnd2  11158  hashf1lem2  11264  zfz1isolemsplit  11268  minmax  11974  xrminmax  12009  fisumrev2  12191  fsumparts  12215  fsumiun  12222  isumnn0nn  12238  fprod2d  12368  fprodle  12385  ege2le3  12416  cos1bnd  12504  efieq1re  12517  eirraplem  12522  3dvds  12609  m1bits  12705  phiprmpw  12978  4sqlem11  13158  4sqlem19  13166  dec5dvds  13169  decsplit1  13185  ballotfilemfval  13207  ballotfilemth  13259  unennn  13266  ennnfonelemjn  13271  qnnen  13300  strle1g  13437  quslem  13622  gsump1  14134  rmodislmod  14660  tgrest  15193  uniretop  15549  cnfldtopn  15563  dvexp  15735  dvef  15751  elply2  15759  cospi  15824  sincos6thpi  15866  logfac  15918  lgsdir2lem2  16062  lgsquadlem2  16111  lgsquad2lem2  16115  2lgsoddprmlem3c  16142  konigsbergumgr  16642  konigsberglem1  16643  konigsberglem2  16644  bj-omind  16874