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 ⊢ 𝐴 = 𝐶

This proof depends on syntax axioms:   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used 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  3595  difdifdirss  3612  dfif3  3654  tpidm  3813  dfint2  3972  iunrab  4060  uniiun  4066  intiin  4067  0iin  4071  mptv  4228  xpundi  4831  xpundir  4832  resiun2  5083  resopab  5107  mptresid  5117  dfse2  5160  cnvun  5193  cnvin  5195  imaundir  5201  imainrect  5233  cnvcnv2  5241  cnvcnvres  5251  dmtpop  5263  rnsnopg  5266  rnco2  5295  dmco  5296  co01  5302  unidmrn  5320  dfdm2  5322  funimaexg  5465  dfmpt3  5506  mptun  5515  funcocnv2  5664  fnasrn  5887  fnasrng  5889  fpr  5897  fmptap  5905  riotav  6044  dmoprab  6169  rnoprab2  6172  mpov  6178  mpomptx  6179  abrexex2g  6349  abrexex2  6353  1stval2  6389  2ndval2  6390  fo1st  6391  fo2nd  6392  xp2  6407  dfoprab4f  6427  fmpoco  6452  tposmpo  6552  recsfval  6586  frecfnom  6672  freccllem  6673  frecfcllem  6675  frecsuclem  6677  df2o3  6702  o1p1e2  6741  ecqs  6871  qliftf  6894  erovlem  6901  fset0  6949  mapsnf1o3  6979  ixp0x  7008  xpf1o  7144  djuunr  7407  dmaddpq  7747  dmmulpq  7748  enq0enq  7799  nqprlu  7915  m1p1sr  8128  m1m1sr  8129  caucvgsr  8170  dfcnqs  8209  3m1e2  9427  2p2e4  9434  3p2e5  9449  3p3e6  9450  4p2e6  9451  4p3e7  9452  4p4e8  9453  5p2e7  9454  5p3e8  9455  5p4e9  9456  6p2e8  9457  6p3e9  9458  7p2e9  9459  nn0supp  9624  nnzrab  9673  nn0zrab  9674  dec0u  9807  dec0h  9808  decsuc  9817  decsucc  9827  numma  9830  decma  9837  decmac  9838  decma2c  9839  decadd  9840  decaddc  9841  decmul1  9850  decmul1c  9851  decmul2c  9852  5p5e10  9857  6p4e10  9858  7p3e10  9861  8p2e10  9866  5t5e25  9889  6t6e36  9894  8t6e48  9905  nn0uz  9967  nnuz  9968  xaddcom  10274  ioomax  10361  iccmax  10362  ioopos  10363  ioorp  10364  fseq1p1m1  10512  fzo0to2pr  10647  fzo0to3tp  10648  frecfzennn  10878  irec  11091  sq10e99m1  11167  facnn  11181  fac0  11182  faclbnd2  11196  hashf1lem2  11302  zfz1isolemsplit  11306  minmax  12014  xrminmax  12050  fisumrev2  12232  fsumparts  12256  fsumiun  12263  isumnn0nn  12279  fprod2d  12409  fprodle  12426  ege2le3  12457  cos1bnd  12545  efieq1re  12558  eirraplem  12563  3dvds  12650  m1bits  12746  phiprmpw  13023  4sqlem11  13203  4sqlem19  13211  dec5dvds  13214  decsplit1  13231  5prm  13246  7prm  13248  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilemfval  13281  ballotfilemth  13333  unennn  13340  ennnfonelemjn  13345  qnnen  13374  strle1g  13513  quslem  13698  elcntr  14157  cntri  14159  cntrsubgnsg  14169  cntrnsg  14170  gsump1  14241  rmodislmod  14772  tgrest  15361  uniretop  15717  cnfldtopn  15731  dvexp  15903  dvef  15919  elply2  15927  cospi  15993  sincos6thpi  16035  logfac  16090  log2ublem3  16184  birthdaylog2  16189  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  ppi2  16235  ppi3  16236  ppiqub  16254  chtqub  16257  bclbnd  16268  bposlem8  16279  lgsdir2lem2  16314  lgsquadlem2  16363  lgsquad2lem2  16367  2lgsoddprmlem3c  16394  konigsbergumgr  16894  konigsberglem1  16895  konigsberglem2  16896  bj-omind  17126