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 2742	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  3eqtr3g  2796  csbeq1a  3907  ss2abdv  4060  ssdifeq0  4486  pofun  5606  opabbi2dv  5848  cnvsng  6220  csbpredg  6304  funcnvpr  6608  funcnvtp  6609  funcnvqp  6610  fresin  6758  fresaunres2  6761  f1imacnv  6847  foimacnv  6848  funfv  6976  dffv2  6984  fimacnvinrn  7071  rescnvimafod  7073  fsn2  7131  funiunfvf  7245  fcof1oinvd  7288  riotaxfrd  7397  f1opw2  7658  fnexALT  7934  fparlem3  8097  fparlem4  8098  fsplitfpar  8101  fvproj  8117  mpocurryd  8251  seqomlem1  8447  seqomlem4  8450  oasuc  8521  oesuclem  8522  omsuc  8523  onasuc  8525  onmsuc  8526  eqerlem  8734  pmresg  8861  fopwdom  9077  sbthlem8  9087  sbthlem9  9088  fodomr  9125  domss2  9133  mapen  9138  cnvfi  9177  enp1iOLD  9277  xpfiOLD  9315  fiint  9321  f1opwfi  9353  mapfien  9400  marypha1lem  9425  unxpwdom  9581  cantnfval2  9661  ttrcltr  9708  infxpenlem  10005  djuinf  10180  isf34lem3  10367  isf34lem5  10370  axdc4lem  10447  ttukeylem6  10506  rankcf  10769  tskuni  10775  gruima  10794  dmrecnq  10960  ltexnq  10967  reclem3pr  11041  pn0sr  11093  mulgt0sr  11097  recdiv  11917  2resupmax  13164  max0sub  13172  rexmul  13247  xmulmnf1  13252  xmulm1  13257  prunioo  13455  fseq1p1m1  13572  fzshftral  13586  seqp1d  13980  seqf1olem2  14005  seqfeq4  14014  binom3  14184  expmulnbnd  14195  discr  14200  bcn2  14276  hashun2  14340  hashun3  14341  hashdif  14370  hashgt12el  14379  hashgt12el2  14380  hashfacen  14410  hashfacenOLD  14411  s2prop  14855  s4prop  14858  s3sndisj  14911  s3iunsndisj  14912  cnrecnv  15109  rddif  15284  amgm2  15313  rlimres  15499  lo1res  15500  iseraltlem2  15626  iseralt  15628  fsumss  15668  fsumcl2lem  15674  isumclim3  15702  fsumcnv  15716  telfsumo  15745  fsumiun  15764  arisum2  15804  geoisum1c  15823  fprodss  15889  fprodser  15890  fprodcl2lem  15891  fprodsplit  15907  fprodn0  15920  fprodcnv  15924  iprodclim3  15941  risefac1  15974  fallfac1  15975  bpolyval  15990  bpoly3  15999  bpoly4  16000  fsumcube  16001  sinhval  16094  cos01bnd  16126  ruclem6  16175  sadadd2lem2  16388  eucalgval  16516  pcid  16803  prmreclem4  16849  4sqlem15  16889  4sqlem16  16890  ramcl  16959  strfv2d  17132  setsid  17138  imasvscafn  17480  xpsff1o  17510  xpsaddlem  17516  xpsvsca  17520  xpsle  17522  mreexexlem2d  17586  mreexexlem4d  17588  sscres  17767  xpcid  18138  evlfcllem  18171  hofcl  18209  isacs5lem  18495  frmdup3lem  18744  cayleylem2  19276  f1omvdco2  19311  symggen  19333  psgnunilem1  19356  pgp0  19459  sylow3lem2  19491  lsmdisjr  19547  lsmdisj2r  19548  subgdisj2  19555  efgval  19580  frgpuplem  19635  frgpup2  19639  gsumval3  19770  gsumzres  19772  gsum2d2lem  19836  dprdf1  19898  dmdprdsplit2lem  19910  dmdprdsplit2  19911  ablfaclem3  19952  prdsmgp  20126  unitgrp  20190  subdrgint  20412  crng2idl  20870  gsumfsum  21005  chrid  21071  znleval  21102  frgpcyg  21121  ocv1  21224  frlmip  21325  ellspd  21349  psrass1lemOLD  21485  psrass1lem  21488  evl1var  21847  pf1mpf  21863  pf1ind  21866  mamuvs2  21898  madurid  22138  baspartn  22449  mretopd  22588  ordtcld1  22693  ordtcld2  22694  leordtvallem1  22706  leordtvallem2  22707  paste  22790  imacmp  22893  cmpsub  22896  unconn  22925  1stckgen  23050  ptbasfi  23077  txcld  23099  ptclsg  23111  txdis1cn  23131  ptrescn  23135  hausdiag  23141  txkgen  23148  xkoptsub  23150  xkococnlem  23155  cnmpt21  23167  cnmpt22  23170  tgqtop  23208  qtoprest  23213  kqdisj  23228  hmeores  23267  hmphindis  23293  pt1hmeo  23302  ptuncnv  23303  ptunhmeo  23304  xpstopnlem1  23305  xkohmeo  23311  alexsublem  23540  ptcmplem2  23549  tmdcn2  23585  cldsubg  23607  qustgplem  23617  tsmsres  23640  ustbas2  23722  ressuss  23759  metreslem  23860  xpsdsval  23879  prdsxmslem2  24030  txmetcnp  24048  tngngp  24163  nrmtngdist  24166  remetdval  24297  cnheibor  24463  evth2  24468  pcoass  24532  ncvspi  24665  iscmet3  24802  rrxip  24899  minveclem2  24935  cmmbl  25043  nulmbl2  25045  volinun  25055  voliunlem1  25059  volsup  25065  ovolioo  25077  uniiccdif  25087  uniioombllem2  25092  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  ismbf3d  25163  itg2uba  25253  itg2i1fseq  25265  itgsplitioo  25347  limcflf  25390  cnplimc  25396  limcun  25404  dvfval  25406  dvres  25420  dvres3a  25423  dvnp1  25434  dvn1  25435  dvexp3  25487  dvsincos  25490  mvth  25501  c1lip2  25507  dvfsumlem2  25536  itgsubstlem  25557  itgsubst  25558  coeeq2  25748  dgreq0  25771  dgrcolem2  25780  vieta1  25817  ulm2  25889  radcnv0  25920  abelthlem2  25936  tanarg  26119  advlogexp  26155  efopn  26158  logtayl  26160  cxpcn3  26246  ang180lem3  26306  quad2  26334  mcubic  26342  binom4  26345  dquart  26348  quart1lem  26350  quart1  26351  quartlem1  26352  asinlem3a  26365  efiatan  26407  tanatan  26414  atanbndlem  26420  dvatan  26430  wilthlem2  26563  ftalem3  26569  ftalem5  26571  basellem3  26577  mumullem2  26674  musum  26685  chtublem  26704  perfectlem2  26723  bposlem6  26782  bposlem9  26785  1lgs  26833  lgs1  26834  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgsquadlem2  26874  lgsquad2lem2  26878  2sqblem  26924  rpvmasum2  27005  log2sumbnd  27037  noetasuplem4  27229  sltlpss  27391  opphllem3  27990  vtxdun  28728  clwwlknon2num  29348  eucrct2eupth  29488  ex-fpar  29705  nvpi  29908  nvop  29917  phop  30059  minvecolem2  30116  hi01  30337  pjchi  30673  chjidm  30761  mayete3i  30969  ho0val  30991  lnop0  31207  adjbdlnb  31325  pjin2i  31434  mdslmd3i  31573  mdexchi  31576  imadifxp  31820  fcoinver  31823  suppovss  31894  fressupp  31898  supppreima  31901  mptprop  31908  padct  31932  f1od2  31934  fcobijfs  31936  ffsrn  31942  iocinif  31980  difioo  31981  s2rn  32098  s3rn  32100  cshw1s2  32112  gsummpt2co  32188  gsumhashmul  32196  symgfcoeu  32231  symgcom  32232  pmtrprfv2  32237  pmtrcnel2  32239  tocyc01  32265  cycpmconjv  32289  cycpmconjs  32303  ofldchr  32421  lsmsnorb2  32491  krull  32583  opprqusbas  32591  opprqusplusg  32592  qsdrngi  32598  ply1chr  32650  rgmoddimOLD  32684  ply1degltdimlem  32696  lindsun  32699  dimkerim  32701  fldexttr  32726  smatlem  32766  zarcmplem  32850  indf1ofs  33013  esumpad2  33043  hasheuni  33072  esumcvg2  33074  esum2dlem  33079  sigapildsys  33149  measxun2  33197  measunl  33203  measinblem  33207  carsgclctunlem1  33305  carsgclctunlem3  33308  sibfof  33328  sitgclg  33330  eulerpartlemgf  33367  probdif  33408  cndprobval  33421  ballotlemic  33494  signsvtn0  33570  signstres  33575  chtvalz  33630  hgt750lemd  33649  bnj1415  34038  f1resrcmplf1d  34079  f1resfz0f1d  34092  revwlk  34104  subfacp1lem1  34159  subfacp1lem3  34162  subfacp1lem5  34164  cvmscld  34253  cvmlift2lem9a  34283  cvmlift2lem9  34291  fwddifnp1  35126  gg-dvfsumlem2  35172  finxpreclem5  36265  ptrest  36476  poimirlem2  36479  poimirlem3  36480  poimirlem6  36483  poimirlem7  36484  poimirlem9  36486  poimirlem11  36488  poimirlem12  36489  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem24  36501  poimirlem25  36502  poimirlem27  36504  poimirlem28  36505  poimirlem29  36506  poimirlem31  36508  voliunnfl  36521  volsupnfl  36522  mbfresfi  36523  itg2addnclem2  36529  itg2addnclem3  36530  ftc1anclem5  36554  dvacos  36562  areacirclem5  36569  cocnv  36582  istotbnd3  36628  ssbnd  36645  disjresdisj  37096  eccnvepres3  37143  symrelim  37418  osumcllem9N  38824  4atexlemex2  38931  cdleme20j  39178  cdlemg47  39596  diaintclN  39918  dibintclN  40027  dihintcl  40204  lclkrlem2e  40371  lclkrlem2p  40382  lcfrlem31  40433  lcmineqlem  40906  sticksstones8  40958  evlsvvval  41133  selvvvval  41155  fsuppssind  41163  readdlid  41273  prjspnval2  41357  flt4lem  41384  diophin  41496  monotuz  41666  monotoddzzfi  41667  oddcomabszz  41669  fnwe2val  41777  lnmlmic  41816  fiuneneq  41925  cytpval  41937  oaun3  42118  ntrkbimka  42775  ntrneifv2  42817  mnringmulrd  42966  mnringmulrcld  42973  radcnvrat  43059  nzprmdif  43064  binomcxplemnotnn0  43101  ioccncflimc  44588  icocncflimc  44592  stoweidlem50  44753  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem107  44916  elsprel  46130  reuopreuprim  46181  perfectALTVlem2  46377  restclssep  47502  seposep  47512  iscnrm3rlem8  47534  logb2aval  47763  aacllem  47802