Theorem eqtr4i 2255

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtr2i  2258  3eqtr2ri  2259  3eqtr4i  2262  3eqtr4ri  2263  rabab  2825  cbvralcsf  3191  cbvrexcsf  3192  cbvrabcsf  3194  dfin5  3208  dfdif2  3209  uneqin  3460  unrab  3480  inrab  3481  inrab2  3482  difrab  3483  dfrab3ss  3487  rabun2  3488  difidALT  3566  difdifdirss  3581  dfif3  3623  tpidm  3777  dfint2  3935  iunrab  4023  uniiun  4029  intiin  4030  0iin  4034  mptv  4191  xpundi  4788  xpundir  4789  resiun2  5039  resopab  5063  mptresid  5073  dfse2  5116  cnvun  5149  cnvin  5151  imaundir  5157  imainrect  5189  cnvcnv2  5197  cnvcnvres  5207  dmtpop  5219  rnsnopg  5222  rnco2  5251  dmco  5252  co01  5258  unidmrn  5276  dfdm2  5278  funimaexg  5421  dfmpt3  5462  mptun  5471  funcocnv2  5617  fnasrn  5834  fnasrng  5836  fpr  5844  fmptap  5852  riotav  5987  dmoprab  6112  rnoprab2  6115  mpov  6121  mpomptx  6122  abrexex2g  6291  abrexex2  6295  1stval2  6327  2ndval2  6328  fo1st  6329  fo2nd  6330  xp2  6345  dfoprab4f  6365  fmpoco  6390  tposmpo  6490  recsfval  6524  frecfnom  6610  freccllem  6611  frecfcllem  6613  frecsuclem  6615  df2o3  6640  o1p1e2  6679  ecqs  6809  qliftf  6832  erovlem  6839  mapsnf1o3  6909  ixp0x  6938  xpf1o  7073  djuunr  7308  dmaddpq  7642  dmmulpq  7643  enq0enq  7694  nqprlu  7810  m1p1sr  8023  m1m1sr  8024  caucvgsr  8065  dfcnqs  8104  3m1e2  9305  2p2e4  9312  3p2e5  9327  3p3e6  9328  4p2e6  9329  4p3e7  9330  4p4e8  9331  5p2e7  9332  5p3e8  9333  5p4e9  9334  6p2e8  9335  6p3e9  9336  7p2e9  9337  nn0supp  9498  nnzrab  9547  nn0zrab  9548  dec0u  9675  dec0h  9676  decsuc  9685  decsucc  9695  numma  9698  decma  9705  decmac  9706  decma2c  9707  decadd  9708  decaddc  9709  decmul1  9718  decmul1c  9719  decmul2c  9720  5p5e10  9725  6p4e10  9726  7p3e10  9729  8p2e10  9734  5t5e25  9757  6t6e36  9762  8t6e48  9773  nn0uz  9835  nnuz  9836  xaddcom  10140  ioomax  10227  iccmax  10228  ioopos  10229  ioorp  10230  fseq1p1m1  10374  fzo0to2pr  10509  fzo0to3tp  10510  frecfzennn  10734  irec  10947  sq10e99m1  11021  facnn  11035  fac0  11036  faclbnd2  11050  zfz1isolemsplit  11148  minmax  11853  xrminmax  11888  fisumrev2  12070  fsumparts  12094  fsumiun  12101  isumnn0nn  12117  fprod2d  12247  fprodle  12264  ege2le3  12295  cos1bnd  12383  efieq1re  12396  eirraplem  12401  3dvds  12488  m1bits  12584  phiprmpw  12857  4sqlem11  13037  4sqlem19  13045  dec5dvds  13048  decsplit1  13064  unennn  13081  ennnfonelemjn  13086  qnnen  13115  strle1g  13252  quslem  13470  rmodislmod  14430  tgrest  14963  uniretop  15319  cnfldtopn  15333  dvexp  15505  dvef  15521  elply2  15529  cospi  15594  sincos6thpi  15636  lgsdir2lem2  15831  lgsquadlem2  15880  lgsquad2lem2  15884  2lgsoddprmlem3c  15911  konigsbergumgr  16411  konigsberglem1  16412  konigsberglem2  16413  bj-omind  16633  gfsump1  16798