Theorem eqtr4i 2262

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

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  7406  dmaddpq  7746  dmmulpq  7747  enq0enq  7798  nqprlu  7914  m1p1sr  8127  m1m1sr  8128  caucvgsr  8169  dfcnqs  8208  3m1e2  9426  2p2e4  9433  3p2e5  9448  3p3e6  9449  4p2e6  9450  4p3e7  9451  4p4e8  9452  5p2e7  9453  5p3e8  9454  5p4e9  9455  6p2e8  9456  6p3e9  9457  7p2e9  9458  nn0supp  9623  nnzrab  9672  nn0zrab  9673  dec0u  9806  dec0h  9807  decsuc  9816  decsucc  9826  numma  9829  decma  9836  decmac  9837  decma2c  9838  decadd  9839  decaddc  9840  decmul1  9849  decmul1c  9850  decmul2c  9851  5p5e10  9856  6p4e10  9857  7p3e10  9860  8p2e10  9865  5t5e25  9888  6t6e36  9893  8t6e48  9904  nn0uz  9966  nnuz  9967  xaddcom  10273  ioomax  10360  iccmax  10361  ioopos  10362  ioorp  10363  fseq1p1m1  10511  fzo0to2pr  10646  fzo0to3tp  10647  frecfzennn  10876  irec  11089  sq10e99m1  11165  facnn  11179  fac0  11180  faclbnd2  11194  hashf1lem2  11300  zfz1isolemsplit  11304  minmax  12011  xrminmax  12047  fisumrev2  12229  fsumparts  12253  fsumiun  12260  isumnn0nn  12276  fprod2d  12406  fprodle  12423  ege2le3  12454  cos1bnd  12542  efieq1re  12555  eirraplem  12560  3dvds  12647  m1bits  12743  phiprmpw  13020  4sqlem11  13200  4sqlem19  13208  dec5dvds  13211  decsplit1  13228  5prm  13243  7prm  13245  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  1259prm  13267  ballotfilemfval  13278  ballotfilemth  13330  unennn  13337  ennnfonelemjn  13342  qnnen  13371  strle1g  13509  quslem  13694  gsump1  14206  rmodislmod  14737  tgrest  15319  uniretop  15675  cnfldtopn  15689  dvexp  15861  dvef  15877  elply2  15885  cospi  15951  sincos6thpi  15993  logfac  16048  log2ublem3  16142  birthdaylog2  16147  ppiprm  16170  ppinprm  16171  ppi2  16179  ppi3  16180  ppiqub  16194  bclbnd  16205  lgsdir2lem2  16246  lgsquadlem2  16295  lgsquad2lem2  16299  2lgsoddprmlem3c  16326  konigsbergumgr  16826  konigsberglem1  16827  konigsberglem2  16828  bj-omind  17058