Theorem eqtr4i 2220

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr2i  2223  3eqtr2ri  2224  3eqtr4i  2227  3eqtr4ri  2228  rabab  2784  cbvralcsf  3147  cbvrexcsf  3148  cbvrabcsf  3150  dfin5  3164  dfdif2  3165  uneqin  3415  unrab  3435  inrab  3436  inrab2  3437  difrab  3438  dfrab3ss  3442  rabun2  3443  difidALT  3521  difdifdirss  3536  dfif3  3575  tpidm  3725  dfint2  3877  iunrab  3965  uniiun  3971  intiin  3972  0iin  3976  mptv  4131  xpundi  4720  xpundir  4721  resiun2  4967  resopab  4991  mptresid  5001  dfse2  5043  cnvun  5076  cnvin  5078  imaundir  5084  imainrect  5116  cnvcnv2  5124  cnvcnvres  5134  dmtpop  5146  rnsnopg  5149  rnco2  5178  dmco  5179  co01  5185  unidmrn  5203  dfdm2  5205  funimaexg  5343  dfmpt3  5383  mptun  5392  funcocnv2  5532  fnasrn  5743  fnasrng  5745  fpr  5747  fmptap  5755  riotav  5886  dmoprab  6007  rnoprab2  6010  mpov  6016  mpomptx  6017  abrexex2g  6186  abrexex2  6190  1stval2  6222  2ndval2  6223  fo1st  6224  fo2nd  6225  xp2  6240  dfoprab4f  6260  fmpoco  6283  tposmpo  6348  recsfval  6382  frecfnom  6468  freccllem  6469  frecfcllem  6471  frecsuclem  6473  df2o3  6497  o1p1e2  6535  ecqs  6665  qliftf  6688  erovlem  6695  mapsnf1o3  6765  ixp0x  6794  xpf1o  6914  djuunr  7141  dmaddpq  7465  dmmulpq  7466  enq0enq  7517  nqprlu  7633  m1p1sr  7846  m1m1sr  7847  caucvgsr  7888  dfcnqs  7927  3m1e2  9129  2p2e4  9136  3p2e5  9151  3p3e6  9152  4p2e6  9153  4p3e7  9154  4p4e8  9155  5p2e7  9156  5p3e8  9157  5p4e9  9158  6p2e8  9159  6p3e9  9160  7p2e9  9161  nn0supp  9320  nnzrab  9369  nn0zrab  9370  dec0u  9496  dec0h  9497  decsuc  9506  decsucc  9516  numma  9519  decma  9526  decmac  9527  decma2c  9528  decadd  9529  decaddc  9530  decmul1  9539  decmul1c  9540  decmul2c  9541  5p5e10  9546  6p4e10  9547  7p3e10  9550  8p2e10  9555  5t5e25  9578  6t6e36  9583  8t6e48  9594  nn0uz  9655  nnuz  9656  xaddcom  9955  ioomax  10042  iccmax  10043  ioopos  10044  ioorp  10045  fseq1p1m1  10188  fzo0to2pr  10313  fzo0to3tp  10314  frecfzennn  10537  irec  10750  sq10e99m1  10824  facnn  10838  fac0  10839  faclbnd2  10853  zfz1isolemsplit  10949  minmax  11414  xrminmax  11449  fisumrev2  11630  fsumparts  11654  fsumiun  11661  isumnn0nn  11677  fprod2d  11807  fprodle  11824  ege2le3  11855  cos1bnd  11943  efieq1re  11956  eirraplem  11961  3dvds  12048  m1bits  12144  phiprmpw  12417  4sqlem11  12597  4sqlem19  12605  dec5dvds  12608  decsplit1  12624  unennn  12641  ennnfonelemjn  12646  qnnen  12675  strle1g  12811  quslem  13028  rmodislmod  13985  tgrest  14513  uniretop  14869  cnfldtopn  14883  dvexp  15055  dvef  15071  elply2  15079  cospi  15144  sincos6thpi  15186  lgsdir2lem2  15378  lgsquadlem2  15427  lgsquad2lem2  15431  2lgsoddprmlem3c  15458  bj-omind  15688