Theorem eqtr3id 2784

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  3eqtr3g  2793  csbeq1a  3906  ss2abdv  4059  ssdifeq0  4485  pofun  5605  opabbi2dv  5848  cnvsng  6221  csbpredg  6305  funcnvpr  6609  funcnvtp  6610  funcnvqp  6611  fresin  6759  fresaunres2  6762  f1imacnv  6848  foimacnv  6849  funfv  6977  dffv2  6985  fimacnvinrn  7072  rescnvimafod  7074  fsn2  7135  funiunfvf  7250  fcof1oinvd  7293  riotaxfrd  7402  f1opw2  7663  fnexALT  7939  fparlem3  8102  fparlem4  8103  fsplitfpar  8106  fvproj  8122  mpocurryd  8256  seqomlem1  8452  seqomlem4  8455  oasuc  8526  oesuclem  8527  omsuc  8528  onasuc  8530  onmsuc  8531  eqerlem  8739  pmresg  8866  fopwdom  9082  sbthlem8  9092  sbthlem9  9093  fodomr  9130  domss2  9138  mapen  9143  cnvfi  9182  enp1iOLD  9282  xpfiOLD  9320  fiint  9326  f1opwfi  9358  mapfien  9405  marypha1lem  9430  unxpwdom  9586  cantnfval2  9666  ttrcltr  9713  infxpenlem  10010  djuinf  10185  isf34lem3  10372  isf34lem5  10375  axdc4lem  10452  ttukeylem6  10511  rankcf  10774  tskuni  10780  gruima  10799  dmrecnq  10965  ltexnq  10972  reclem3pr  11046  pn0sr  11098  mulgt0sr  11102  recdiv  11924  2resupmax  13171  max0sub  13179  rexmul  13254  xmulmnf1  13259  xmulm1  13264  prunioo  13462  fseq1p1m1  13579  fzshftral  13593  seqp1d  13987  seqf1olem2  14012  seqfeq4  14021  binom3  14191  expmulnbnd  14202  discr  14207  bcn2  14283  hashun2  14347  hashun3  14348  hashdif  14377  hashgt12el  14386  hashgt12el2  14387  hashfacen  14417  hashfacenOLD  14418  s2prop  14862  s4prop  14865  s3sndisj  14918  s3iunsndisj  14919  cnrecnv  15116  rddif  15291  amgm2  15320  rlimres  15506  lo1res  15507  iseraltlem2  15633  iseralt  15635  fsumss  15675  fsumcl2lem  15681  isumclim3  15709  fsumcnv  15723  telfsumo  15752  fsumiun  15771  arisum2  15811  geoisum1c  15830  fprodss  15896  fprodser  15897  fprodcl2lem  15898  fprodsplit  15914  fprodn0  15927  fprodcnv  15931  iprodclim3  15948  risefac1  15981  fallfac1  15982  bpolyval  15997  bpoly3  16006  bpoly4  16007  fsumcube  16008  sinhval  16101  cos01bnd  16133  ruclem6  16182  sadadd2lem2  16395  eucalgval  16523  pcid  16810  prmreclem4  16856  4sqlem15  16896  4sqlem16  16897  ramcl  16966  strfv2d  17139  setsid  17145  imasvscafn  17487  xpsff1o  17517  xpsaddlem  17523  xpsvsca  17527  xpsle  17529  mreexexlem2d  17593  mreexexlem4d  17595  sscres  17774  xpcid  18145  evlfcllem  18178  hofcl  18216  isacs5lem  18502  frmdup3lem  18783  cayleylem2  19322  f1omvdco2  19357  symggen  19379  psgnunilem1  19402  pgp0  19505  sylow3lem2  19537  lsmdisjr  19593  lsmdisj2r  19594  subgdisj2  19601  efgval  19626  frgpuplem  19681  frgpup2  19685  gsumval3  19816  gsumzres  19818  gsum2d2lem  19882  dprdf1  19944  dmdprdsplit2lem  19956  dmdprdsplit2  19957  ablfaclem3  19998  prdsmgp  20045  unitgrp  20274  subdrgint  20562  crng2idl  21027  gsumfsum  21212  pzriprnglem6  21255  chrid  21298  znleval  21329  frgpcyg  21348  ocv1  21451  frlmip  21552  ellspd  21576  psrass1lemOLD  21712  psrass1lem  21715  evl1var  22075  pf1mpf  22091  pf1ind  22094  mamuvs2  22126  madurid  22366  baspartn  22677  mretopd  22816  ordtcld1  22921  ordtcld2  22922  leordtvallem1  22934  leordtvallem2  22935  paste  23018  imacmp  23121  cmpsub  23124  unconn  23153  1stckgen  23278  ptbasfi  23305  txcld  23327  ptclsg  23339  txdis1cn  23359  ptrescn  23363  hausdiag  23369  txkgen  23376  xkoptsub  23378  xkococnlem  23383  cnmpt21  23395  cnmpt22  23398  tgqtop  23436  qtoprest  23441  kqdisj  23456  hmeores  23495  hmphindis  23521  pt1hmeo  23530  ptuncnv  23531  ptunhmeo  23532  xpstopnlem1  23533  xkohmeo  23539  alexsublem  23768  ptcmplem2  23777  tmdcn2  23813  cldsubg  23835  qustgplem  23845  tsmsres  23868  ustbas2  23950  ressuss  23987  metreslem  24088  xpsdsval  24107  prdsxmslem2  24258  txmetcnp  24276  tngngp  24391  nrmtngdist  24394  remetdval  24525  cnheibor  24701  evth2  24706  pcoass  24771  ncvspi  24904  iscmet3  25041  rrxip  25138  minveclem2  25174  cmmbl  25283  nulmbl2  25285  volinun  25295  voliunlem1  25299  volsup  25305  ovolioo  25317  uniiccdif  25327  uniioombllem2  25332  uniioombllem3  25334  uniioombllem4  25335  uniioombllem5  25336  ismbf3d  25403  itg2uba  25493  itg2i1fseq  25505  itgsplitioo  25587  limcflf  25630  cnplimc  25636  limcun  25644  dvfval  25646  dvres  25660  dvres3a  25663  dvnp1  25675  dvn1  25676  dvexp3  25730  dvsincos  25733  mvth  25744  c1lip2  25750  dvfsumlem2  25779  itgsubstlem  25800  itgsubst  25801  coeeq2  25991  dgreq0  26015  dgrcolem2  26024  vieta1  26061  ulm2  26133  radcnv0  26164  abelthlem2  26180  tanarg  26363  advlogexp  26399  efopn  26402  logtayl  26404  cxpcn3  26492  ang180lem3  26552  quad2  26580  mcubic  26588  binom4  26591  dquart  26594  quart1lem  26596  quart1  26597  quartlem1  26598  asinlem3a  26611  efiatan  26653  tanatan  26660  atanbndlem  26666  dvatan  26676  wilthlem2  26809  ftalem3  26815  ftalem5  26817  basellem3  26823  mumullem2  26920  musum  26931  chtublem  26950  perfectlem2  26969  bposlem6  27028  bposlem9  27031  1lgs  27079  lgs1  27080  lgseisenlem1  27114  lgseisenlem2  27115  lgseisenlem3  27116  lgsquadlem2  27120  lgsquad2lem2  27124  2sqblem  27170  rpvmasum2  27251  log2sumbnd  27283  noetasuplem4  27475  sltlpss  27638  slelss  27639  opphllem3  28267  vtxdun  29005  clwwlknon2num  29625  eucrct2eupth  29765  ex-fpar  29982  nvpi  30187  nvop  30196  phop  30338  minvecolem2  30395  hi01  30616  pjchi  30952  chjidm  31040  mayete3i  31248  ho0val  31270  lnop0  31486  adjbdlnb  31604  pjin2i  31713  mdslmd3i  31852  mdexchi  31855  imadifxp  32099  fcoinver  32102  suppovss  32173  fressupp  32177  supppreima  32180  mptprop  32187  padct  32211  f1od2  32213  fcobijfs  32215  ffsrn  32221  iocinif  32259  difioo  32260  s2rn  32377  s3rn  32379  cshw1s2  32391  gsummpt2co  32470  gsumhashmul  32478  symgfcoeu  32513  symgcom  32514  pmtrprfv2  32519  pmtrcnel2  32521  tocyc01  32547  cycpmconjv  32571  cycpmconjs  32585  ofldchr  32702  lsmsnorb2  32776  krull  32868  opprqusbas  32876  opprqusplusg  32877  qsdrngi  32883  ply1chr  32935  rgmoddimOLD  32983  ply1degltdimlem  32995  lindsun  32998  dimkerim  33000  fldexttr  33025  smatlem  33075  zarcmplem  33159  indf1ofs  33322  esumpad2  33352  hasheuni  33381  esumcvg2  33383  esum2dlem  33388  sigapildsys  33458  measxun2  33506  measunl  33512  measinblem  33516  carsgclctunlem1  33614  carsgclctunlem3  33617  sibfof  33637  sitgclg  33639  eulerpartlemgf  33676  probdif  33717  cndprobval  33730  ballotlemic  33803  signsvtn0  33879  signstres  33884  chtvalz  33939  hgt750lemd  33958  bnj1415  34347  f1resrcmplf1d  34388  f1resfz0f1d  34401  revwlk  34413  subfacp1lem1  34468  subfacp1lem3  34471  subfacp1lem5  34473  cvmscld  34562  cvmlift2lem9a  34592  cvmlift2lem9  34600  fwddifnp1  35441  gg-dvfsumlem2  35469  finxpreclem5  36579  ptrest  36790  poimirlem2  36793  poimirlem3  36794  poimirlem6  36797  poimirlem7  36798  poimirlem9  36800  poimirlem11  36802  poimirlem12  36803  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem24  36815  poimirlem25  36816  poimirlem27  36818  poimirlem28  36819  poimirlem29  36820  poimirlem31  36822  voliunnfl  36835  volsupnfl  36836  mbfresfi  36837  itg2addnclem2  36843  itg2addnclem3  36844  ftc1anclem5  36868  dvacos  36876  areacirclem5  36883  cocnv  36896  istotbnd3  36942  ssbnd  36959  disjresdisj  37410  eccnvepres3  37457  symrelim  37732  osumcllem9N  39138  4atexlemex2  39245  cdleme20j  39492  cdlemg47  39910  diaintclN  40232  dibintclN  40341  dihintcl  40518  lclkrlem2e  40685  lclkrlem2p  40696  lcfrlem31  40747  lcmineqlem  41223  sticksstones8  41275  evlsvvval  41437  selvvvval  41459  fsuppssind  41467  readdlid  41578  prjspnval2  41662  flt4lem  41689  diophin  41812  monotuz  41982  monotoddzzfi  41983  oddcomabszz  41985  fnwe2val  42093  lnmlmic  42132  fiuneneq  42241  cytpval  42253  oaun3  42434  ntrkbimka  43091  ntrneifv2  43133  mnringmulrd  43282  mnringmulrcld  43289  radcnvrat  43375  nzprmdif  43380  binomcxplemnotnn0  43417  ioccncflimc  44899  icocncflimc  44903  stoweidlem50  45064  fourierdlem89  45209  fourierdlem90  45210  fourierdlem91  45211  fourierdlem107  45227  elsprel  46441  reuopreuprim  46492  perfectALTVlem2  46688  restclssep  47635  seposep  47645  iscnrm3rlem8  47667  logb2aval  47896  aacllem  47935