Theorem syl5eq 2126

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5eq.1	⊢ 𝐴 = 𝐵
syl5eq.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
syl5eq	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		syl5eq.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrd 2114	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  syl5req  2127  syl5eqr  2128  3eqtr3a  2138  3eqtr4g  2139  csbtt  2919  csbvarg  2934  csbie2g  2953  rabbi2dva  3175  csbprc  3290  disjssun  3308  disjpr2  3458  prprc2  3503  difprsn2  3528  opprc  3593  intsng  3672  riinm  3752  iinxsng  3753  rintm  3767  sucprc  4169  unisucg  4171  xpriindim  4496  relop  4508  dmxpm  4577  riinint  4615  resabs1  4662  resabs2  4663  resima2  4666  xpssres  4667  resopab2  4679  imasng  4714  ndmima  4726  xpdisj1  4771  xpdisj2  4772  djudisj  4774  resdisj  4775  rnxpm  4776  xpima1  4791  xpima2m  4792  dmsnsnsng  4822  rnsnopg  4823  rnpropg  4824  mptiniseg  4839  dfco2a  4845  relcoi1  4873  unixpm  4877  iotaval  4902  funtp  4977  fnun  5030  fnresdisj  5034  fnima  5042  fnimaeq0  5045  fcoi1  5095  f1orescnv  5167  foun  5170  resdif  5173  tz6.12-2  5194  fveu  5195  tz6.12-1  5226  fvun2  5266  fvopab3ig  5272  f1oresrab  5355  dfmptg  5368  ressnop0  5370  fvunsng  5383  fsnunfv  5389  fvpr1  5391  fvpr2  5392  fvpr1g  5393  fvpr2g  5394  fvtp1g  5395  fvtp2g  5396  fvtp3g  5397  fvtp2  5399  fvtp3  5400  f1oiso2  5491  riotaund  5527  ovprc  5565  resoprab2  5623  fnoprabg  5627  ovidig  5643  ovigg  5646  ov6g  5663  ovconst2  5677  offval2  5751  ot1stg  5804  ot2ndg  5805  ot3rdgg  5806  fmpt2co  5862  algrflemg  5876  tpostpos2  5908  rdgisuc1  6027  frec0g  6040  frecsuclem  6049  frecrdg  6051  oasuc  6102  oa1suc  6105  omsuc  6109  nnm1  6156  nnm2  6157  dfec2  6168  errn  6187  phplem2  6378  undiffi  6433  eqinfti  6482  infvalti  6484  infsnti  6492  1qec  6629  mulidnq  6630  addpinq1  6705  0idsr  6995  1idsr  6996  caucvgsrlemoffres  7027  caucvgsr  7029  mulresr  7057  pitonnlem2  7066  ax1rid  7094  axcnre  7098  negid  7411  subneg  7413  negneg  7414  dfinfre  8090  2times  8216  infrenegsupex  8752  rexneg  8962  fseq1p1m1  9176  fzosplitprm1  9309  intfracq  9391  frec2uz0d  9470  frec2uzrdg  9480  frecuzrdg0  9484  frecuzrdgg  9487  frecuzrdg0t  9493  iseqval  9519  iseqvalt  9521  sqval  9620  iexpcyc  9665  binom3  9676  faclbnd  9754  faclbnd2  9755  bcn1  9771  sizeinf  9791  sizeennn  9793  shftlem  9831  shftuz  9832  shftidt  9848  reim0  9875  remullem  9885  resqrexlemf1  10021  resqrexlemcalc3  10029  absexpzap  10093  absimle  10097  amgm2  10131  minmax  10239  ialgr0  10559  ialgrp1  10561  eucialg  10574  ex-ceil  10700  qdencn  10928