Theorem eqtr3id 2812

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

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  3eqtr3g  2821  csbeq1a  3867  ssdifeq0  4447  pofun  5587  opabbi2dv  5835  cnvsng  6224  csbpredg  6308  funcnvpr  6598  funcnvtp  6599  funcnvqp  6600  fresin  6747  fresaunres2  6750  f1imacnv  6837  foimacnv  6838  funfv  6968  dffv2  6976  fimacnvinrn  7066  rescnvimafod  7068  fsn2  7132  funiunfvf  7247  fcof1oinvd  7291  riotaxfrd  7401  f1opw2  7665  fnexALT  7944  fparlem3  8105  fparlem4  8106  fsplitfpar  8109  fvproj  8126  mpocurryd  8261  seqomlem1  8433  seqomlem4  8436  oasuc  8505  oesuclem  8506  omsuc  8507  onasuc  8509  onmsuc  8510  eqerlem  8726  pmresg  8864  fopwdom  9069  sbthlem8  9078  sbthlem9  9079  fodomr  9112  domss2  9120  mapen  9125  cnvfi  9156  fiint  9282  fodomfir  9283  f1opwfi  9309  mapfien  9364  marypha1lem  9389  unxpwdom  9547  cantnfval2  9634  ttrcltr  9681  infxpenlem  9993  djuinf  10168  isf34lem3  10354  isf34lem5  10357  axdc4lem  10434  ttukeylem6  10493  rankcf  10757  tskuni  10763  gruima  10782  dmrecnq  10948  ltexnq  10955  reclem3pr  11029  pn0sr  11081  mulgt0sr  11085  recdiv  11916  2resupmax  13209  max0sub  13217  rexmul  13292  xmulmnf1  13297  xmulm1  13302  prunioo  13503  fseq1p1m1  13622  fzshftral  13639  seqp1d  14050  seqf1olem2  14074  seqfeq4  14083  binom3  14256  expmulnbnd  14267  discr  14272  bcn2  14351  hashun2  14415  hashun3  14416  hashdif  14446  hashgt12el  14455  hashgt12el2  14456  hashfacen  14487  s2prop  14940  s4prop  14943  s3sndisj  15000  s3iunsndisj  15001  cnrecnv  15212  rddif  15388  amgm2  15417  rlimres  15605  lo1res  15606  iseraltlem2  15730  iseralt  15732  fsumss  15772  fsumcl2lem  15778  isumclim3  15806  fsumcnv  15820  telfsumo  15850  fsumiun  15869  arisum2  15911  geoisum1c  15930  fprodss  15998  fprodser  15999  fprodcl2lem  16000  fprodsplit  16016  fprodn0  16029  fprodcnv  16033  iprodclim3  16050  risefac1  16082  fallfac1  16083  bpolyval  16098  bpoly3  16107  bpoly4  16108  fsumcube  16109  sinhval  16205  cos01bnd  16237  ruclem6  16286  sadadd2lem2  16503  eucalgval  16635  pcid  16928  prmreclem4  16974  4sqlem15  17014  4sqlem16  17015  ramcl  17084  strfv2d  17256  setsid  17262  imasvscafn  17586  xpsff1o  17616  xpsaddlem  17622  xpsvsca  17626  xpsle  17628  mreexexlem2d  17696  mreexexlem4d  17698  sscres  17875  xpcid  18240  evlfcllem  18272  hofcl  18310  isacs5lem  18596  frmdup3lem  18920  cayleylem2  19478  f1omvdco2  19513  symggen  19535  psgnunilem1  19558  pgp0  19661  sylow3lem2  19693  lsmdisjr  19749  lsmdisj2r  19750  subgdisj2  19757  efgval  19782  frgpuplem  19837  frgpup2  19841  gsumval3  19972  gsumzres  19974  gsum2d2lem  20038  dprdf1  20100  dmdprdsplit2lem  20112  dmdprdsplit2  20113  ablfaclem3  20154  prdsmgp  20222  unitgrp  20461  subdrgint  20906  crng2idl  21420  gsumfsum  21584  pzriprnglem6  21636  chrid  21675  znleval  21704  frgpcyg  21723  ofldchr  21726  ocv1  21829  frlmip  21928  ellspd  21952  psrass1lem  22083  evlsvvval  22244  selvvvval  22293  ply1chr  22466  evl1var  22496  pf1mpf  22512  pf1ind  22515  mamuvs2  22563  madurid  22801  baspartn  23111  mretopd  23249  ordtcld1  23354  ordtcld2  23355  leordtvallem1  23367  leordtvallem2  23368  paste  23451  imacmp  23554  cmpsub  23557  unconn  23586  1stckgen  23711  ptbasfi  23738  txcld  23760  ptclsg  23772  txdis1cn  23792  ptrescn  23796  hausdiag  23802  txkgen  23809  xkoptsub  23811  xkococnlem  23816  cnmpt21  23828  cnmpt22  23831  tgqtop  23869  qtoprest  23874  kqdisj  23889  hmeores  23928  hmphindis  23954  pt1hmeo  23963  ptuncnv  23964  ptunhmeo  23965  xpstopnlem1  23966  xkohmeo  23972  alexsublem  24201  ptcmplem2  24210  tmdcn2  24246  cldsubg  24268  qustgplem  24278  tsmsres  24301  ustbas2  24382  ressuss  24419  metreslem  24519  xpsdsval  24538  prdsxmslem2  24686  txmetcnp  24704  tngngp  24811  nrmtngdist  24814  remetdval  24946  cnheibor  25114  evth2  25119  pcoass  25183  ncvspi  25315  iscmet3  25452  rrxip  25549  minveclem2  25585  cmmbl  25693  nulmbl2  25695  volinun  25705  voliunlem1  25709  volsup  25715  ovolioo  25727  uniiccdif  25737  uniioombllem2  25742  uniioombllem3  25744  uniioombllem4  25745  uniioombllem5  25746  ismbf3d  25813  itg2uba  25902  itg2i1fseq  25914  itgsplitioo  25997  limcflf  26040  cnplimc  26046  limcun  26054  dvfval  26056  dvres  26070  dvres3a  26073  dvnp1  26084  dvn1  26085  dvexp3  26137  dvsincos  26140  mvth  26151  c1lip2  26157  dvfsumlem2  26186  itgsubstlem  26207  itgsubst  26208  coeeq2  26399  dgreq0  26422  dgrcolem2  26431  vieta1  26473  ulm2  26548  radcnv0  26579  abelthlem2  26595  tanarg  26784  advlogexp  26820  efopn  26823  logtayl  26825  cxpcn3  26913  ang180lem3  26976  quad2  27004  mcubic  27012  binom4  27015  dquart  27018  quart1lem  27020  quart1  27021  quartlem1  27022  asinlem3a  27035  efiatan  27077  tanatan  27084  atanbndlem  27090  dvatan  27100  wilthlem2  27233  ftalem3  27239  ftalem5  27241  basellem3  27247  mumullem2  27344  musum  27355  mpodvdsmulf1o  27358  chtublem  27375  perfectlem2  27394  bposlem6  27453  bposlem9  27456  1lgs  27504  lgs1  27505  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgsquadlem2  27545  lgsquad2lem2  27549  2sqblem  27595  rpvmasum2  27676  log2sumbnd  27708  noetasuplem4  27900  ltslpss  28101  leslss  28102  bdayfinbndlem1  28660  z12shalf  28673  opphllem3  29030  prlngpln3  29199  vtxdun  29831  clwwlknon2num  30456  eucrct2eupth  30596  ex-fpar  30813  nvpi  31019  nvop  31028  phop  31170  minvecolem2  31227  hi01  31448  pjchi  31784  chjidm  31872  mayete3i  32080  ho0val  32102  lnop0  32318  adjbdlnb  32436  pjin2i  32545  mdslmd3i  32684  mdexchi  32687  imadifxp  32946  fcoinver  32949  suppovss  33026  fressupp  33033  supppreima  33036  mptprop  33043  f1od2  33064  fcobijfs  33066  ffsrn  33073  iocinif  33126  difioo  33127  indf1ofs  33186  s2rnOLD  33264  s3rnOLD  33266  cshw1s2  33280  gsummpt2co  33368  gsumhashmul  33387  gsummulsubdishift1s  33390  gsummulsubdishift2s  33391  symgfcoeu  33402  symgcom  33403  pmtrprfv2  33408  pmtrcnel2  33410  tocyc01  33438  cycpmconjv  33462  cycpmconjs  33476  elrgspnlem2  33563  lsmsnorb2  33705  krull  33761  opprqusbas  33770  opprqusplusg  33771  qsdrngi  33777  psrgsum  33938  psrmonprod  33942  ply1degltdimlem  34012  lindsun  34015  dimkerim  34017  fldexttr  34048  constrcon  34164  cos9thpiminplylem3  34174  smatlem  34187  zarcmplem  34271  esumpad2  34446  hasheuni  34475  esumcvg2  34477  esum2dlem  34482  sigapildsys  34552  measxun2  34600  measunl  34606  measinblem  34610  carsgclctunlem1  34707  carsgclctunlem3  34710  sibfof  34730  sitgclg  34732  eulerpartlemgf  34769  probdif  34810  cndprobval  34823  ballotlemic  34897  signsvtn0  34957  signstres  34962  chtvalz  35016  hgt750lemd  35035  bnj1415  35426  f1resrcmplf1d  35475  f1resfz0f1d  35605  revwlk  35617  subfacp1lem1  35671  subfacp1lem3  35674  subfacp1lem5  35676  cvmscld  35765  cvmlift2lem9a  35795  cvmlift2lem9  35803  fwddifnp1  36657  dfttc4  37041  finxpreclem5  38041  ptrest  38270  poimirlem2  38273  poimirlem3  38274  poimirlem6  38277  poimirlem7  38278  poimirlem9  38280  poimirlem11  38282  poimirlem12  38283  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem24  38295  poimirlem25  38296  poimirlem27  38298  poimirlem28  38299  poimirlem29  38300  poimirlem31  38302  voliunnfl  38315  volsupnfl  38316  mbfresfi  38317  itg2addnclem2  38323  itg2addnclem3  38324  ftc1anclem5  38348  dvacos  38356  areacirclem5  38363  cocnv  38376  istotbnd3  38422  ssbnd  38439  disjresdisj  38893  eccnvepres3  38941  dfblockliftmap2  39110  symrelim  39292  osumcllem9N  40738  4atexlemex2  40845  cdleme20j  41092  cdlemg47  41510  diaintclN  41832  dibintclN  41941  dihintcl  42118  lclkrlem2e  42285  lclkrlem2p  42296  lcfrlem31  42347  lcmineqlem  42819  sticksstones8  42920  dvun  43120  readdlid  43164  fsuppssind  43325  prjspnval2  43350  flt4lem  43377  diophin  43503  monotuz  43668  monotoddzzfi  43669  oddcomabszz  43671  fnwe2val  43776  lnmlmic  43815  fiuneneq  43919  cytpval  43929  oaun3  44109  ntrkbimka  44764  ntrneifv2  44806  mnringmulrd  44947  mnringmulrcld  44952  radcnvrat  45024  nzprmdif  45029  binomcxplemnotnn0  45066  limsupvaluz  46422  ioccncflimc  46599  icocncflimc  46603  stoweidlem50  46764  fourierdlem48  46868  fourierdlem49  46869  fourierdlem89  46909  fourierdlem90  46910  fourierdlem91  46911  fourierdlem107  46927  lambert0  47624  lamberte  47625  elsprel  48224  reuopreuprim  48275  perfectALTVlem2  48487  dfnbgr6  48622  dfsclnbgr6  48623  smprngprmrng  49104  restclssep  49694  seposep  49704  iscnrm3rlem8  49725  swapfid  50057  cofuswapf1  50072  cofuswapf2  50073  idfudiag1lem  50301  termcfuncval  50310  ranval  50398  lmddu  50445  initocmd  50447  logb2aval  50542  aacllem  50621