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  3906  ss2abdv  4059  ssdifeq0  4485  pofun  5605  opabbi2dv  5847  cnvsng  6219  csbpredg  6303  funcnvpr  6607  funcnvtp  6608  funcnvqp  6609  fresin  6757  fresaunres2  6760  f1imacnv  6846  foimacnv  6847  funfv  6974  dffv2  6982  fimacnvinrn  7069  rescnvimafod  7071  fsn2  7129  funiunfvf  7243  fcof1oinvd  7286  riotaxfrd  7395  f1opw2  7656  fnexALT  7932  fparlem3  8095  fparlem4  8096  fsplitfpar  8099  fvproj  8115  mpocurryd  8249  seqomlem1  8445  seqomlem4  8448  oasuc  8519  oesuclem  8520  omsuc  8521  onasuc  8523  onmsuc  8524  eqerlem  8733  pmresg  8860  fopwdom  9076  sbthlem8  9086  sbthlem9  9087  fodomr  9124  domss2  9132  mapen  9137  cnvfi  9176  enp1iOLD  9276  xpfiOLD  9314  fiint  9320  f1opwfi  9352  mapfien  9399  marypha1lem  9424  unxpwdom  9580  cantnfval2  9660  ttrcltr  9707  infxpenlem  10004  djuinf  10179  isf34lem3  10366  isf34lem5  10369  axdc4lem  10446  ttukeylem6  10505  rankcf  10768  tskuni  10774  gruima  10793  dmrecnq  10959  ltexnq  10966  reclem3pr  11040  pn0sr  11092  mulgt0sr  11096  recdiv  11916  2resupmax  13163  max0sub  13171  rexmul  13246  xmulmnf1  13251  xmulm1  13256  prunioo  13454  fseq1p1m1  13571  fzshftral  13585  seqp1d  13979  seqf1olem2  14004  seqfeq4  14013  binom3  14183  expmulnbnd  14194  discr  14199  bcn2  14275  hashun2  14339  hashun3  14340  hashdif  14369  hashgt12el  14378  hashgt12el2  14379  hashfacen  14409  hashfacenOLD  14410  s2prop  14854  s4prop  14857  s3sndisj  14910  s3iunsndisj  14911  cnrecnv  15108  rddif  15283  amgm2  15312  rlimres  15498  lo1res  15499  iseraltlem2  15625  iseralt  15627  fsumss  15667  fsumcl2lem  15673  isumclim3  15701  fsumcnv  15715  telfsumo  15744  fsumiun  15763  arisum2  15803  geoisum1c  15822  fprodss  15888  fprodser  15889  fprodcl2lem  15890  fprodsplit  15906  fprodn0  15919  fprodcnv  15923  iprodclim3  15940  risefac1  15973  fallfac1  15974  bpolyval  15989  bpoly3  15998  bpoly4  15999  fsumcube  16000  sinhval  16093  cos01bnd  16125  ruclem6  16174  sadadd2lem2  16387  eucalgval  16515  pcid  16802  prmreclem4  16848  4sqlem15  16888  4sqlem16  16889  ramcl  16958  strfv2d  17131  setsid  17137  imasvscafn  17479  xpsff1o  17509  xpsaddlem  17515  xpsvsca  17519  xpsle  17521  mreexexlem2d  17585  mreexexlem4d  17587  sscres  17766  xpcid  18137  evlfcllem  18170  hofcl  18208  isacs5lem  18494  frmdup3lem  18743  cayleylem2  19274  f1omvdco2  19309  symggen  19331  psgnunilem1  19354  pgp0  19457  sylow3lem2  19489  lsmdisjr  19545  lsmdisj2r  19546  subgdisj2  19553  efgval  19578  frgpuplem  19633  frgpup2  19637  gsumval3  19767  gsumzres  19769  gsum2d2lem  19833  dprdf1  19895  dmdprdsplit2lem  19907  dmdprdsplit2  19908  ablfaclem3  19949  prdsmgp  20122  unitgrp  20186  subdrgint  20407  crng2idl  20864  gsumfsum  20997  chrid  21063  znleval  21094  frgpcyg  21113  ocv1  21216  frlmip  21317  ellspd  21341  psrass1lemOLD  21475  psrass1lem  21478  evl1var  21837  pf1mpf  21853  pf1ind  21856  mamuvs2  21888  madurid  22128  baspartn  22439  mretopd  22578  ordtcld1  22683  ordtcld2  22684  leordtvallem1  22696  leordtvallem2  22697  paste  22780  imacmp  22883  cmpsub  22886  unconn  22915  1stckgen  23040  ptbasfi  23067  txcld  23089  ptclsg  23101  txdis1cn  23121  ptrescn  23125  hausdiag  23131  txkgen  23138  xkoptsub  23140  xkococnlem  23145  cnmpt21  23157  cnmpt22  23160  tgqtop  23198  qtoprest  23203  kqdisj  23218  hmeores  23257  hmphindis  23283  pt1hmeo  23292  ptuncnv  23293  ptunhmeo  23294  xpstopnlem1  23295  xkohmeo  23301  alexsublem  23530  ptcmplem2  23539  tmdcn2  23575  cldsubg  23597  qustgplem  23607  tsmsres  23630  ustbas2  23712  ressuss  23749  metreslem  23850  xpsdsval  23869  prdsxmslem2  24020  txmetcnp  24038  tngngp  24153  nrmtngdist  24156  remetdval  24287  cnheibor  24453  evth2  24458  pcoass  24522  ncvspi  24655  iscmet3  24792  rrxip  24889  minveclem2  24925  cmmbl  25033  nulmbl2  25035  volinun  25045  voliunlem1  25049  volsup  25055  ovolioo  25067  uniiccdif  25077  uniioombllem2  25082  uniioombllem3  25084  uniioombllem4  25085  uniioombllem5  25086  ismbf3d  25153  itg2uba  25243  itg2i1fseq  25255  itgsplitioo  25337  limcflf  25380  cnplimc  25386  limcun  25394  dvfval  25396  dvres  25410  dvres3a  25413  dvnp1  25424  dvn1  25425  dvexp3  25477  dvsincos  25480  mvth  25491  c1lip2  25497  dvfsumlem2  25526  itgsubstlem  25547  itgsubst  25548  coeeq2  25738  dgreq0  25761  dgrcolem2  25770  vieta1  25807  ulm2  25879  radcnv0  25910  abelthlem2  25926  tanarg  26109  advlogexp  26145  efopn  26148  logtayl  26150  cxpcn3  26236  ang180lem3  26296  quad2  26324  mcubic  26332  binom4  26335  dquart  26338  quart1lem  26340  quart1  26341  quartlem1  26342  asinlem3a  26355  efiatan  26397  tanatan  26404  atanbndlem  26410  dvatan  26420  wilthlem2  26553  ftalem3  26559  ftalem5  26561  basellem3  26567  mumullem2  26664  musum  26675  chtublem  26694  perfectlem2  26713  bposlem6  26772  bposlem9  26775  1lgs  26823  lgs1  26824  lgseisenlem1  26858  lgseisenlem2  26859  lgseisenlem3  26860  lgsquadlem2  26864  lgsquad2lem2  26868  2sqblem  26914  rpvmasum2  26995  log2sumbnd  27027  noetasuplem4  27219  sltlpss  27381  opphllem3  27980  vtxdun  28718  clwwlknon2num  29338  eucrct2eupth  29478  ex-fpar  29695  nvpi  29898  nvop  29907  phop  30049  minvecolem2  30106  hi01  30327  pjchi  30663  chjidm  30751  mayete3i  30959  ho0val  30981  lnop0  31197  adjbdlnb  31315  pjin2i  31424  mdslmd3i  31563  mdexchi  31566  imadifxp  31810  fcoinver  31813  suppovss  31884  fressupp  31888  supppreima  31891  mptprop  31898  padct  31922  f1od2  31924  fcobijfs  31926  ffsrn  31932  iocinif  31970  difioo  31971  s2rn  32088  s3rn  32090  cshw1s2  32102  gsummpt2co  32178  gsumhashmul  32186  symgfcoeu  32221  symgcom  32222  pmtrprfv2  32227  pmtrcnel2  32229  tocyc01  32255  cycpmconjv  32279  cycpmconjs  32293  ofldchr  32401  lsmsnorb2  32467  krull  32547  opprqusbas  32555  opprqusplusg  32556  qsdrngi  32562  ply1chr  32608  rgmoddim  32640  ply1degltdimlem  32652  lindsun  32655  dimkerim  32657  fldexttr  32682  smatlem  32715  zarcmplem  32799  indf1ofs  32962  esumpad2  32992  hasheuni  33021  esumcvg2  33023  esum2dlem  33028  sigapildsys  33098  measxun2  33146  measunl  33152  measinblem  33156  carsgclctunlem1  33254  carsgclctunlem3  33257  sibfof  33277  sitgclg  33279  eulerpartlemgf  33316  probdif  33357  cndprobval  33370  ballotlemic  33443  signsvtn0  33519  signstres  33524  chtvalz  33579  hgt750lemd  33598  bnj1415  33987  f1resrcmplf1d  34028  f1resfz0f1d  34041  revwlk  34053  subfacp1lem1  34108  subfacp1lem3  34111  subfacp1lem5  34113  cvmscld  34202  cvmlift2lem9a  34232  cvmlift2lem9  34240  fwddifnp1  35075  gg-dvfsumlem2  35121  finxpreclem5  36214  ptrest  36425  poimirlem2  36428  poimirlem3  36429  poimirlem6  36432  poimirlem7  36433  poimirlem9  36435  poimirlem11  36437  poimirlem12  36438  poimirlem16  36442  poimirlem17  36443  poimirlem19  36445  poimirlem20  36446  poimirlem24  36450  poimirlem25  36451  poimirlem27  36453  poimirlem28  36454  poimirlem29  36455  poimirlem31  36457  voliunnfl  36470  volsupnfl  36471  mbfresfi  36472  itg2addnclem2  36478  itg2addnclem3  36479  ftc1anclem5  36503  dvacos  36511  areacirclem5  36518  cocnv  36531  istotbnd3  36577  ssbnd  36594  disjresdisj  37045  eccnvepres3  37092  symrelim  37367  osumcllem9N  38773  4atexlemex2  38880  cdleme20j  39127  cdlemg47  39545  diaintclN  39867  dibintclN  39976  dihintcl  40153  lclkrlem2e  40320  lclkrlem2p  40331  lcfrlem31  40382  lcmineqlem  40855  sticksstones8  40907  evlsvvval  41085  selvvvval  41107  fsuppssind  41115  readdlid  41220  prjspnval2  41304  flt4lem  41331  diophin  41443  monotuz  41613  monotoddzzfi  41614  oddcomabszz  41616  fnwe2val  41724  lnmlmic  41763  fiuneneq  41872  cytpval  41884  oaun3  42065  ntrkbimka  42722  ntrneifv2  42764  mnringmulrd  42913  mnringmulrcld  42920  radcnvrat  43006  nzprmdif  43011  binomcxplemnotnn0  43048  ioccncflimc  44536  icocncflimc  44540  stoweidlem50  44701  fourierdlem89  44846  fourierdlem90  44847  fourierdlem91  44848  fourierdlem107  44864  elsprel  46078  reuopreuprim  46129  perfectALTVlem2  46325  restclssep  47450  seposep  47460  iscnrm3rlem8  47482  logb2aval  47711  aacllem  47750