Theorem eqtr4i 2199

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

Syntax hints:   = wceq 1353

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  3eqtr2i  2202  3eqtr2ri  2203  3eqtr4i  2206  3eqtr4ri  2207  rabab  2756  cbvralcsf  3117  cbvrexcsf  3118  cbvrabcsf  3120  dfin5  3134  dfdif2  3135  uneqin  3384  unrab  3404  inrab  3405  inrab2  3406  difrab  3407  dfrab3ss  3411  rabun2  3412  difidALT  3490  difdifdirss  3505  dfif3  3545  tpidm  3691  dfint2  3842  iunrab  3929  uniiun  3935  intiin  3936  0iin  3940  mptv  4095  xpundi  4676  xpundir  4677  resiun2  4920  resopab  4944  opabresid  4953  dfse2  4994  cnvun  5026  cnvin  5028  imaundir  5034  imainrect  5066  cnvcnv2  5074  cnvcnvres  5084  dmtpop  5096  rnsnopg  5099  rnco2  5128  dmco  5129  co01  5135  unidmrn  5153  dfdm2  5155  funimaexg  5292  dfmpt3  5330  mptun  5339  funcocnv2  5478  fnasrn  5686  fnasrng  5688  fpr  5690  fmptap  5698  riotav  5826  dmoprab  5946  rnoprab2  5949  mpov  5955  mpomptx  5956  abrexex2g  6111  abrexex2  6115  1stval2  6146  2ndval2  6147  fo1st  6148  fo2nd  6149  xp2  6164  dfoprab4f  6184  fmpoco  6207  tposmpo  6272  recsfval  6306  frecfnom  6392  freccllem  6393  frecfcllem  6395  frecsuclem  6397  df2o3  6421  o1p1e2  6459  ecqs  6587  qliftf  6610  erovlem  6617  mapsnf1o3  6687  ixp0x  6716  xpf1o  6834  djuunr  7055  dmaddpq  7353  dmmulpq  7354  enq0enq  7405  nqprlu  7521  m1p1sr  7734  m1m1sr  7735  caucvgsr  7776  dfcnqs  7815  3m1e2  9010  2p2e4  9017  3p2e5  9031  3p3e6  9032  4p2e6  9033  4p3e7  9034  4p4e8  9035  5p2e7  9036  5p3e8  9037  5p4e9  9038  6p2e8  9039  6p3e9  9040  7p2e9  9041  nn0supp  9199  nnzrab  9248  nn0zrab  9249  dec0u  9375  dec0h  9376  decsuc  9385  decsucc  9395  numma  9398  decma  9405  decmac  9406  decma2c  9407  decadd  9408  decaddc  9409  decmul1  9418  decmul1c  9419  decmul2c  9420  5p5e10  9425  6p4e10  9426  7p3e10  9429  8p2e10  9434  5t5e25  9457  6t6e36  9462  8t6e48  9473  nn0uz  9533  nnuz  9534  xaddcom  9830  ioomax  9917  iccmax  9918  ioopos  9919  ioorp  9920  fseq1p1m1  10062  fzo0to2pr  10186  fzo0to3tp  10187  frecfzennn  10394  irec  10587  sq10e99m1  10659  facnn  10673  fac0  10674  faclbnd2  10688  zfz1isolemsplit  10784  minmax  11204  xrminmax  11239  fisumrev2  11420  fsumparts  11444  fsumiun  11451  isumnn0nn  11467  fprod2d  11597  fprodle  11614  ege2le3  11645  cos1bnd  11733  efieq1re  11745  eirraplem  11750  phiprmpw  12187  unennn  12363  ennnfonelemjn  12368  qnnen  12397  strle1g  12519  tgrest  13220  uniretop  13576  dvexp  13726  dvef  13739  cospi  13772  sincos6thpi  13814  lgsdir2lem2  13981  bj-omind  14226