Theorem eqtr4i 2253

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 2233	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2250	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr2i  2256  3eqtr2ri  2257  3eqtr4i  2260  3eqtr4ri  2261  rabab  2821  cbvralcsf  3187  cbvrexcsf  3188  cbvrabcsf  3190  dfin5  3204  dfdif2  3205  uneqin  3455  unrab  3475  inrab  3476  inrab2  3477  difrab  3478  dfrab3ss  3482  rabun2  3483  difidALT  3561  difdifdirss  3576  dfif3  3616  tpidm  3768  dfint2  3925  iunrab  4013  uniiun  4019  intiin  4020  0iin  4024  mptv  4181  xpundi  4775  xpundir  4776  resiun2  5025  resopab  5049  mptresid  5059  dfse2  5101  cnvun  5134  cnvin  5136  imaundir  5142  imainrect  5174  cnvcnv2  5182  cnvcnvres  5192  dmtpop  5204  rnsnopg  5207  rnco2  5236  dmco  5237  co01  5243  unidmrn  5261  dfdm2  5263  funimaexg  5405  dfmpt3  5446  mptun  5455  funcocnv2  5599  fnasrn  5815  fnasrng  5817  fpr  5825  fmptap  5833  riotav  5966  dmoprab  6091  rnoprab2  6094  mpov  6100  mpomptx  6101  abrexex2g  6271  abrexex2  6275  1stval2  6307  2ndval2  6308  fo1st  6309  fo2nd  6310  xp2  6325  dfoprab4f  6345  fmpoco  6368  tposmpo  6433  recsfval  6467  frecfnom  6553  freccllem  6554  frecfcllem  6556  frecsuclem  6558  df2o3  6583  o1p1e2  6622  ecqs  6752  qliftf  6775  erovlem  6782  mapsnf1o3  6852  ixp0x  6881  xpf1o  7013  djuunr  7244  dmaddpq  7577  dmmulpq  7578  enq0enq  7629  nqprlu  7745  m1p1sr  7958  m1m1sr  7959  caucvgsr  8000  dfcnqs  8039  3m1e2  9241  2p2e4  9248  3p2e5  9263  3p3e6  9264  4p2e6  9265  4p3e7  9266  4p4e8  9267  5p2e7  9268  5p3e8  9269  5p4e9  9270  6p2e8  9271  6p3e9  9272  7p2e9  9273  nn0supp  9432  nnzrab  9481  nn0zrab  9482  dec0u  9609  dec0h  9610  decsuc  9619  decsucc  9629  numma  9632  decma  9639  decmac  9640  decma2c  9641  decadd  9642  decaddc  9643  decmul1  9652  decmul1c  9653  decmul2c  9654  5p5e10  9659  6p4e10  9660  7p3e10  9663  8p2e10  9668  5t5e25  9691  6t6e36  9696  8t6e48  9707  nn0uz  9769  nnuz  9770  xaddcom  10069  ioomax  10156  iccmax  10157  ioopos  10158  ioorp  10159  fseq1p1m1  10302  fzo0to2pr  10436  fzo0to3tp  10437  frecfzennn  10660  irec  10873  sq10e99m1  10947  facnn  10961  fac0  10962  faclbnd2  10976  zfz1isolemsplit  11073  minmax  11756  xrminmax  11791  fisumrev2  11972  fsumparts  11996  fsumiun  12003  isumnn0nn  12019  fprod2d  12149  fprodle  12166  ege2le3  12197  cos1bnd  12285  efieq1re  12298  eirraplem  12303  3dvds  12390  m1bits  12486  phiprmpw  12759  4sqlem11  12939  4sqlem19  12947  dec5dvds  12950  decsplit1  12966  unennn  12983  ennnfonelemjn  12988  qnnen  13017  strle1g  13154  quslem  13372  rmodislmod  14330  tgrest  14858  uniretop  15214  cnfldtopn  15228  dvexp  15400  dvef  15416  elply2  15424  cospi  15489  sincos6thpi  15531  lgsdir2lem2  15723  lgsquadlem2  15772  lgsquad2lem2  15776  2lgsoddprmlem3c  15803  bj-omind  16352