Theorem eqtr3id 2807

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

Hypotheses

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

Assertion

Ref	Expression
eqtr3id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr3id

Step	Hyp	Ref	Expression
1		eqtr3id.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2767	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5eq 2805	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750

This theorem is referenced by:  3eqtr3g  2816  csbeq1a  3821  ss2abdv  3970  ssdifeq0  4383  pofun  5464  opabbi2dv  5695  cnvsng  6057  funcnvpr  6402  funcnvtp  6403  funcnvqp  6404  fresin  6537  fresaunres2  6540  f1imacnv  6623  foimacnv  6624  funfv  6744  dffv2  6752  fimacnvinrn  6837  fsn2  6895  funiunfvf  7006  fcof1oinvd  7047  riotaxfrd  7148  f1opw2  7402  fnexALT  7662  fparlem3  7820  fparlem4  7821  fsplitfpar  7825  fvproj  7839  mpocurryd  7951  seqomlem1  8102  seqomlem4  8105  oasuc  8165  oesuclem  8166  omsuc  8167  onasuc  8169  onmsuc  8170  eqerlem  8339  pmresg  8465  fopwdom  8659  sbthlem8  8669  sbthlem9  8670  fodomr  8703  domss2  8711  mapen  8716  enp1i  8802  xpfi  8835  fiint  8841  f1opwfi  8874  mapfien  8918  marypha1lem  8943  unxpwdom  9099  cantnfval2  9178  infxpenlem  9486  djuinf  9661  isf34lem3  9848  isf34lem5  9851  axdc4lem  9928  ttukeylem6  9987  rankcf  10250  tskuni  10256  gruima  10275  dmrecnq  10441  ltexnq  10448  reclem3pr  10522  pn0sr  10574  mulgt0sr  10578  recdiv  11397  2resupmax  12635  max0sub  12643  rexmul  12718  xmulmnf1  12723  xmulm1  12728  prunioo  12926  fseq1p1m1  13043  fzshftral  13057  seqp1d  13448  seqf1olem2  13473  seqfeq4  13482  binom3  13648  expmulnbnd  13659  discr  13664  bcn2  13742  hashun2  13807  hashun3  13808  hashdif  13837  hashgt12el  13846  hashgt12el2  13847  hashfacen  13875  hashfacenOLD  13876  s2prop  14329  s4prop  14332  s3sndisj  14387  s3iunsndisj  14388  cnrecnv  14585  rddif  14761  amgm2  14790  rlimres  14976  lo1res  14977  iseraltlem2  15100  iseralt  15102  fsumss  15143  fsumcl2lem  15149  isumclim3  15175  fsumcnv  15189  telfsumo  15218  fsumiun  15237  arisum2  15277  geoisum1c  15297  fprodss  15363  fprodser  15364  fprodcl2lem  15365  fprodsplit  15381  fprodn0  15394  fprodcnv  15398  iprodclim3  15415  risefac1  15448  fallfac1  15449  bpolyval  15464  bpoly3  15473  bpoly4  15474  fsumcube  15475  sinhval  15568  cos01bnd  15600  ruclem6  15649  sadadd2lem2  15862  eucalgval  15992  pcid  16278  prmreclem4  16324  4sqlem15  16364  4sqlem16  16365  ramcl  16434  strfv2d  16601  setsid  16610  imasvscafn  16882  xpsff1o  16912  xpsaddlem  16918  xpsvsca  16922  xpsle  16924  mreexexlem2d  16988  mreexexlem4d  16990  sscres  17166  xpcid  17519  evlfcllem  17551  hofcl  17589  isacs5lem  17859  frmdup3lem  18111  cayleylem2  18622  f1omvdco2  18657  symggen  18679  psgnunilem1  18702  pgp0  18802  sylow3lem2  18834  lsmdisjr  18891  lsmdisj2r  18892  subgdisj2  18899  efgval  18924  frgpuplem  18979  frgpup2  18983  gsumval3  19109  gsumzres  19111  gsum2d2lem  19175  dprdf1  19237  dmdprdsplit2lem  19249  dmdprdsplit2  19250  ablfaclem3  19291  prdsmgp  19445  unitgrp  19502  subdrgint  19664  crng2idl  20094  gsumfsum  20247  chrid  20309  znleval  20336  frgpcyg  20355  ocv1  20458  frlmip  20557  ellspd  20581  psrass1lemOLD  20716  psrass1lem  20719  evl1var  21069  pf1mpf  21085  pf1ind  21088  mamuvs2  21120  madurid  21358  baspartn  21668  mretopd  21806  ordtcld1  21911  ordtcld2  21912  leordtvallem1  21924  leordtvallem2  21925  paste  22008  imacmp  22111  cmpsub  22114  unconn  22143  1stckgen  22268  ptbasfi  22295  txcld  22317  ptclsg  22329  txdis1cn  22349  ptrescn  22353  hausdiag  22359  txkgen  22366  xkoptsub  22368  xkococnlem  22373  cnmpt21  22385  cnmpt22  22388  tgqtop  22426  qtoprest  22431  kqdisj  22446  hmeores  22485  hmphindis  22511  pt1hmeo  22520  ptuncnv  22521  ptunhmeo  22522  xpstopnlem1  22523  xkohmeo  22529  alexsublem  22758  ptcmplem2  22767  tmdcn2  22803  cldsubg  22825  qustgplem  22835  tsmsres  22858  ustbas2  22940  ressuss  22978  metreslem  23078  xpsdsval  23097  prdsxmslem2  23245  txmetcnp  23263  tngngp  23370  nrmtngdist  23373  remetdval  23504  cnheibor  23670  evth2  23675  pcoass  23739  ncvspi  23871  iscmet3  24007  rrxip  24104  minveclem2  24140  cmmbl  24248  nulmbl2  24250  volinun  24260  voliunlem1  24264  volsup  24270  ovolioo  24282  uniiccdif  24292  uniioombllem2  24297  uniioombllem3  24299  uniioombllem4  24300  uniioombllem5  24301  ismbf3d  24368  itg2uba  24457  itg2i1fseq  24469  itgsplitioo  24551  limcflf  24594  cnplimc  24600  limcun  24608  dvfval  24610  dvres  24624  dvres3a  24627  dvnp1  24638  dvn1  24639  dvexp3  24691  dvsincos  24694  mvth  24705  c1lip2  24711  dvfsumlem2  24740  itgsubstlem  24761  itgsubst  24762  coeeq2  24952  dgreq0  24975  dgrcolem2  24984  vieta1  25021  ulm2  25093  radcnv0  25124  abelthlem2  25140  tanarg  25323  advlogexp  25359  efopn  25362  logtayl  25364  cxpcn3  25450  ang180lem3  25510  quad2  25538  mcubic  25546  binom4  25549  dquart  25552  quart1lem  25554  quart1  25555  quartlem1  25556  asinlem3a  25569  efiatan  25611  tanatan  25618  atanbndlem  25624  dvatan  25634  wilthlem2  25767  ftalem3  25773  ftalem5  25775  basellem3  25781  mumullem2  25878  musum  25889  chtublem  25908  perfectlem2  25927  bposlem6  25986  bposlem9  25989  1lgs  26037  lgs1  26038  lgseisenlem1  26072  lgseisenlem2  26073  lgseisenlem3  26074  lgsquadlem2  26078  lgsquad2lem2  26082  2sqblem  26128  rpvmasum2  26209  log2sumbnd  26241  opphllem3  26656  vtxdun  27384  clwwlknon2num  28003  eucrct2eupth  28143  ex-fpar  28360  nvpi  28563  nvop  28572  phop  28714  minvecolem2  28771  hi01  28992  pjchi  29328  chjidm  29416  mayete3i  29624  ho0val  29646  lnop0  29862  adjbdlnb  29980  pjin2i  30089  mdslmd3i  30228  mdexchi  30231  imadifxp  30476  fcoinver  30482  fnunres2  30552  suppovss  30554  fressupp  30559  supppreima  30562  mptprop  30568  padct  30591  f1od2  30593  fcobijfs  30595  ffsrn  30601  iocinif  30639  difioo  30640  s2rn  30755  s3rn  30757  cshw1s2  30769  gsummpt2co  30847  gsumhashmul  30855  symgfcoeu  30890  symgcom  30891  pmtrprfv2  30896  pmtrcnel2  30898  tocyc01  30924  cycpmconjv  30948  cycpmconjs  30962  ofldchr  31052  lsmsnorb2  31114  krull  31177  ply1chr  31203  rgmoddim  31227  lindsun  31240  dimkerim  31242  fldexttr  31267  smatlem  31281  zarcmplem  31365  indf1ofs  31526  esumpad2  31556  hasheuni  31585  esumcvg2  31587  esum2dlem  31592  sigapildsys  31662  measxun2  31710  measunl  31716  measinblem  31720  carsgclctunlem1  31816  carsgclctunlem3  31819  sibfof  31839  sitgclg  31841  eulerpartlemgf  31878  probdif  31919  cndprobval  31932  ballotlemic  32005  signsvtn0  32081  signstres  32086  chtvalz  32141  hgt750lemd  32160  bnj1415  32551  f1resrcmplf1d  32592  f1resfz0f1d  32601  revwlk  32615  subfacp1lem1  32670  subfacp1lem3  32673  subfacp1lem5  32675  cvmscld  32764  cvmlift2lem9a  32794  cvmlift2lem9  32802  noetasuplem4  33537  fwddifnp1  34051  csbpredg  35058  finxpreclem5  35127  ptrest  35371  poimirlem2  35374  poimirlem3  35375  poimirlem6  35378  poimirlem7  35379  poimirlem9  35381  poimirlem11  35383  poimirlem12  35384  poimirlem16  35388  poimirlem17  35389  poimirlem19  35391  poimirlem20  35392  poimirlem24  35396  poimirlem25  35397  poimirlem27  35399  poimirlem28  35400  poimirlem29  35401  poimirlem31  35403  voliunnfl  35416  volsupnfl  35417  mbfresfi  35418  itg2addnclem2  35424  itg2addnclem3  35425  ftc1anclem5  35449  dvacos  35457  areacirclem5  35464  cocnv  35478  istotbnd3  35524  ssbnd  35541  eccnvepres3  36017  symrelim  36270  osumcllem9N  37575  4atexlemex2  37682  cdleme20j  37929  cdlemg47  38347  diaintclN  38669  dibintclN  38778  dihintcl  38955  lclkrlem2e  39122  lclkrlem2p  39133  lcfrlem31  39184  lcmineqlem  39654  evlsbagval  39819  fsuppssind  39826  readdid2  39928  prjspnval2  39999  flt4lem  40019  diophin  40131  monotuz  40300  monotoddzzfi  40301  oddcomabszz  40303  fnwe2val  40411  lnmlmic  40450  fiuneneq  40559  cytpval  40571  ntrkbimka  41159  ntrneifv2  41201  mnringmulrd  41349  mnringmulrcld  41354  radcnvrat  41436  nzprmdif  41441  binomcxplemnotnn0  41478  ioccncflimc  42938  icocncflimc  42942  stoweidlem50  43103  fourierdlem89  43248  fourierdlem90  43249  fourierdlem91  43250  fourierdlem107  43266  elsprel  44419  reuopreuprim  44470  perfectALTVlem2  44666  restclssep  45660  seposep  45670  iscnrm3rlem8  45692  logb2aval  45787  aacllem  45826