Theorem eqtr3id 2787

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 2747	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5eq 2785	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730

This theorem is referenced by:  3eqtr3g  2796  csbeq1a  3804  ss2abdv  3953  ssdifeq0  4373  pofun  5460  opabbi2dv  5692  cnvsng  6055  funcnvpr  6401  funcnvtp  6402  funcnvqp  6403  fresin  6547  fresaunres2  6550  f1imacnv  6634  foimacnv  6635  funfv  6755  dffv2  6763  fimacnvinrn  6849  fsn2  6908  funiunfvf  7019  fcof1oinvd  7060  riotaxfrd  7162  f1opw2  7416  fnexALT  7677  fparlem3  7835  fparlem4  7836  fsplitfpar  7840  fvproj  7854  mpocurryd  7964  seqomlem1  8115  seqomlem4  8118  oasuc  8180  oesuclem  8181  omsuc  8182  onasuc  8184  onmsuc  8185  eqerlem  8354  pmresg  8480  fopwdom  8674  sbthlem8  8684  sbthlem9  8685  fodomr  8718  domss2  8726  mapen  8731  cnvfi  8777  enp1i  8830  xpfi  8863  fiint  8869  f1opwfi  8901  mapfien  8945  marypha1lem  8970  unxpwdom  9126  cantnfval2  9205  infxpenlem  9513  djuinf  9688  isf34lem3  9875  isf34lem5  9878  axdc4lem  9955  ttukeylem6  10014  rankcf  10277  tskuni  10283  gruima  10302  dmrecnq  10468  ltexnq  10475  reclem3pr  10549  pn0sr  10601  mulgt0sr  10605  recdiv  11424  2resupmax  12664  max0sub  12672  rexmul  12747  xmulmnf1  12752  xmulm1  12757  prunioo  12955  fseq1p1m1  13072  fzshftral  13086  seqp1d  13477  seqf1olem2  13502  seqfeq4  13511  binom3  13677  expmulnbnd  13688  discr  13693  bcn2  13771  hashun2  13836  hashun3  13837  hashdif  13866  hashgt12el  13875  hashgt12el2  13876  hashfacen  13904  hashfacenOLD  13905  s2prop  14358  s4prop  14361  s3sndisj  14416  s3iunsndisj  14417  cnrecnv  14614  rddif  14790  amgm2  14819  rlimres  15005  lo1res  15006  iseraltlem2  15132  iseralt  15134  fsumss  15175  fsumcl2lem  15181  isumclim3  15207  fsumcnv  15221  telfsumo  15250  fsumiun  15269  arisum2  15309  geoisum1c  15328  fprodss  15394  fprodser  15395  fprodcl2lem  15396  fprodsplit  15412  fprodn0  15425  fprodcnv  15429  iprodclim3  15446  risefac1  15479  fallfac1  15480  bpolyval  15495  bpoly3  15504  bpoly4  15505  fsumcube  15506  sinhval  15599  cos01bnd  15631  ruclem6  15680  sadadd2lem2  15893  eucalgval  16023  pcid  16309  prmreclem4  16355  4sqlem15  16395  4sqlem16  16396  ramcl  16465  strfv2d  16632  setsid  16641  imasvscafn  16913  xpsff1o  16943  xpsaddlem  16949  xpsvsca  16953  xpsle  16955  mreexexlem2d  17019  mreexexlem4d  17021  sscres  17198  xpcid  17555  evlfcllem  17587  hofcl  17625  isacs5lem  17895  frmdup3lem  18147  cayleylem2  18659  f1omvdco2  18694  symggen  18716  psgnunilem1  18739  pgp0  18839  sylow3lem2  18871  lsmdisjr  18928  lsmdisj2r  18929  subgdisj2  18936  efgval  18961  frgpuplem  19016  frgpup2  19020  gsumval3  19146  gsumzres  19148  gsum2d2lem  19212  dprdf1  19274  dmdprdsplit2lem  19286  dmdprdsplit2  19287  ablfaclem3  19328  prdsmgp  19482  unitgrp  19539  subdrgint  19701  crng2idl  20131  gsumfsum  20284  chrid  20346  znleval  20373  frgpcyg  20392  ocv1  20495  frlmip  20594  ellspd  20618  psrass1lemOLD  20753  psrass1lem  20756  evl1var  21106  pf1mpf  21122  pf1ind  21125  mamuvs2  21157  madurid  21395  baspartn  21705  mretopd  21843  ordtcld1  21948  ordtcld2  21949  leordtvallem1  21961  leordtvallem2  21962  paste  22045  imacmp  22148  cmpsub  22151  unconn  22180  1stckgen  22305  ptbasfi  22332  txcld  22354  ptclsg  22366  txdis1cn  22386  ptrescn  22390  hausdiag  22396  txkgen  22403  xkoptsub  22405  xkococnlem  22410  cnmpt21  22422  cnmpt22  22425  tgqtop  22463  qtoprest  22468  kqdisj  22483  hmeores  22522  hmphindis  22548  pt1hmeo  22557  ptuncnv  22558  ptunhmeo  22559  xpstopnlem1  22560  xkohmeo  22566  alexsublem  22795  ptcmplem2  22804  tmdcn2  22840  cldsubg  22862  qustgplem  22872  tsmsres  22895  ustbas2  22977  ressuss  23015  metreslem  23115  xpsdsval  23134  prdsxmslem2  23282  txmetcnp  23300  tngngp  23407  nrmtngdist  23410  remetdval  23541  cnheibor  23707  evth2  23712  pcoass  23776  ncvspi  23908  iscmet3  24045  rrxip  24142  minveclem2  24178  cmmbl  24286  nulmbl2  24288  volinun  24298  voliunlem1  24302  volsup  24308  ovolioo  24320  uniiccdif  24330  uniioombllem2  24335  uniioombllem3  24337  uniioombllem4  24338  uniioombllem5  24339  ismbf3d  24406  itg2uba  24496  itg2i1fseq  24508  itgsplitioo  24590  limcflf  24633  cnplimc  24639  limcun  24647  dvfval  24649  dvres  24663  dvres3a  24666  dvnp1  24677  dvn1  24678  dvexp3  24730  dvsincos  24733  mvth  24744  c1lip2  24750  dvfsumlem2  24779  itgsubstlem  24800  itgsubst  24801  coeeq2  24991  dgreq0  25014  dgrcolem2  25023  vieta1  25060  ulm2  25132  radcnv0  25163  abelthlem2  25179  tanarg  25362  advlogexp  25398  efopn  25401  logtayl  25403  cxpcn3  25489  ang180lem3  25549  quad2  25577  mcubic  25585  binom4  25588  dquart  25591  quart1lem  25593  quart1  25594  quartlem1  25595  asinlem3a  25608  efiatan  25650  tanatan  25657  atanbndlem  25663  dvatan  25673  wilthlem2  25806  ftalem3  25812  ftalem5  25814  basellem3  25820  mumullem2  25917  musum  25928  chtublem  25947  perfectlem2  25966  bposlem6  26025  bposlem9  26028  1lgs  26076  lgs1  26077  lgseisenlem1  26111  lgseisenlem2  26112  lgseisenlem3  26113  lgsquadlem2  26117  lgsquad2lem2  26121  2sqblem  26167  rpvmasum2  26248  log2sumbnd  26280  opphllem3  26695  vtxdun  27423  clwwlknon2num  28042  eucrct2eupth  28182  ex-fpar  28399  nvpi  28602  nvop  28611  phop  28753  minvecolem2  28810  hi01  29031  pjchi  29367  chjidm  29455  mayete3i  29663  ho0val  29685  lnop0  29901  adjbdlnb  30019  pjin2i  30128  mdslmd3i  30267  mdexchi  30270  imadifxp  30514  fcoinver  30520  fnunres2  30590  suppovss  30592  fressupp  30597  supppreima  30600  mptprop  30606  padct  30629  f1od2  30631  fcobijfs  30633  ffsrn  30639  iocinif  30677  difioo  30678  s2rn  30793  s3rn  30795  cshw1s2  30807  gsummpt2co  30885  gsumhashmul  30893  symgfcoeu  30928  symgcom  30929  pmtrprfv2  30934  pmtrcnel2  30936  tocyc01  30962  cycpmconjv  30986  cycpmconjs  31000  ofldchr  31090  lsmsnorb2  31152  krull  31215  ply1chr  31241  rgmoddim  31265  lindsun  31278  dimkerim  31280  fldexttr  31305  smatlem  31319  zarcmplem  31403  indf1ofs  31564  esumpad2  31594  hasheuni  31623  esumcvg2  31625  esum2dlem  31630  sigapildsys  31700  measxun2  31748  measunl  31754  measinblem  31758  carsgclctunlem1  31854  carsgclctunlem3  31857  sibfof  31877  sitgclg  31879  eulerpartlemgf  31916  probdif  31957  cndprobval  31970  ballotlemic  32043  signsvtn0  32119  signstres  32124  chtvalz  32179  hgt750lemd  32198  bnj1415  32589  f1resrcmplf1d  32630  f1resfz0f1d  32643  revwlk  32657  subfacp1lem1  32712  subfacp1lem3  32715  subfacp1lem5  32717  cvmscld  32806  cvmlift2lem9a  32836  cvmlift2lem9  32844  noetasuplem4  33580  sltlpss  33725  fwddifnp1  34105  csbpredg  35120  finxpreclem5  35189  ptrest  35399  poimirlem2  35402  poimirlem3  35403  poimirlem6  35406  poimirlem7  35407  poimirlem9  35409  poimirlem11  35411  poimirlem12  35412  poimirlem16  35416  poimirlem17  35417  poimirlem19  35419  poimirlem20  35420  poimirlem24  35424  poimirlem25  35425  poimirlem27  35427  poimirlem28  35428  poimirlem29  35429  poimirlem31  35431  voliunnfl  35444  volsupnfl  35445  mbfresfi  35446  itg2addnclem2  35452  itg2addnclem3  35453  ftc1anclem5  35477  dvacos  35485  areacirclem5  35492  cocnv  35506  istotbnd3  35552  ssbnd  35569  eccnvepres3  36043  symrelim  36296  osumcllem9N  37601  4atexlemex2  37708  cdleme20j  37955  cdlemg47  38373  diaintclN  38695  dibintclN  38804  dihintcl  38981  lclkrlem2e  39148  lclkrlem2p  39159  lcfrlem31  39210  lcmineqlem  39680  sticksstones8  39715  evlsbagval  39854  fsuppssind  39861  readdid2  39963  prjspnval2  40034  flt4lem  40054  diophin  40166  monotuz  40335  monotoddzzfi  40336  oddcomabszz  40338  fnwe2val  40446  lnmlmic  40485  fiuneneq  40594  cytpval  40606  ntrkbimka  41194  ntrneifv2  41236  mnringmulrd  41383  mnringmulrcld  41388  radcnvrat  41470  nzprmdif  41475  binomcxplemnotnn0  41512  ioccncflimc  42968  icocncflimc  42972  stoweidlem50  43133  fourierdlem89  43278  fourierdlem90  43279  fourierdlem91  43280  fourierdlem107  43296  elsprel  44461  reuopreuprim  44512  perfectALTVlem2  44708  restclssep  45731  seposep  45741  iscnrm3rlem8  45763  logb2aval  45919  aacllem  45958