Theorem eqtr3id 2788

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

Syntax hints:   → wi 4   = wceq 1547

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 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  3eqtr3g  2797  csbeq1a  3845  ssdifeq0  4414  pofun  5544  opabbi2dv  5791  cnvsng  6174  csbpredg  6258  funcnvpr  6547  funcnvtp  6548  funcnvqp  6549  f1imadifssran  6571  fresin  6696  fresaunres2  6699  f1imacnv  6783  foimacnv  6784  funfv  6914  dffv2  6922  fimacnvinrn  7012  rescnvimafod  7014  fsn2  7078  funiunfvf  7193  fcof1oinvd  7237  riotaxfrd  7347  f1opw2  7611  fnexALT  7893  fparlem3  8053  fparlem4  8054  fsplitfpar  8057  fvproj  8074  mpocurryd  8209  seqomlem1  8379  seqomlem4  8382  oasuc  8449  oesuclem  8450  omsuc  8451  onasuc  8453  onmsuc  8454  eqerlem  8669  pmresg  8808  fopwdom  9013  sbthlem8  9022  sbthlem9  9023  fodomr  9056  domss2  9064  mapen  9069  cnvfi  9100  fiint  9227  fodomfir  9228  f1opwfi  9256  mapfien  9311  marypha1lem  9336  unxpwdom  9494  cantnfval2  9581  ttrcltr  9628  infxpenlem  9926  djuinf  10102  isf34lem3  10288  isf34lem5  10291  axdc4lem  10368  ttukeylem6  10427  rankcf  10691  tskuni  10697  gruima  10716  dmrecnq  10882  ltexnq  10889  reclem3pr  10963  pn0sr  11015  mulgt0sr  11019  recdiv  11852  2resupmax  13131  max0sub  13139  rexmul  13214  xmulmnf1  13219  xmulm1  13224  prunioo  13425  fseq1p1m1  13543  fzshftral  13560  seqp1d  13971  seqf1olem2  13995  seqfeq4  14004  binom3  14177  expmulnbnd  14188  discr  14193  bcn2  14272  hashun2  14336  hashun3  14337  hashdif  14366  hashgt12el  14375  hashgt12el2  14376  hashfacen  14407  s2prop  14860  s4prop  14863  s3sndisj  14920  s3iunsndisj  14921  cnrecnv  15118  rddif  15294  amgm2  15323  rlimres  15511  lo1res  15512  iseraltlem2  15636  iseralt  15638  fsumss  15678  fsumcl2lem  15684  isumclim3  15712  fsumcnv  15726  telfsumo  15756  fsumiun  15775  arisum2  15817  geoisum1c  15836  fprodss  15904  fprodser  15905  fprodcl2lem  15906  fprodsplit  15922  fprodn0  15935  fprodcnv  15939  iprodclim3  15956  risefac1  15989  fallfac1  15990  bpolyval  16005  bpoly3  16014  bpoly4  16015  fsumcube  16016  sinhval  16112  cos01bnd  16144  ruclem6  16193  sadadd2lem2  16410  eucalgval  16542  pcid  16835  prmreclem4  16881  4sqlem15  16921  4sqlem16  16922  ramcl  16991  strfv2d  17162  setsid  17168  imasvscafn  17492  xpsff1o  17522  xpsaddlem  17528  xpsvsca  17532  xpsle  17534  mreexexlem2d  17602  mreexexlem4d  17604  sscres  17781  xpcid  18146  evlfcllem  18178  hofcl  18216  isacs5lem  18502  frmdup3lem  18825  cayleylem2  19379  f1omvdco2  19414  symggen  19436  psgnunilem1  19459  pgp0  19562  sylow3lem2  19594  lsmdisjr  19650  lsmdisj2r  19651  subgdisj2  19658  efgval  19683  frgpuplem  19738  frgpup2  19742  gsumval3  19873  gsumzres  19875  gsum2d2lem  19939  dprdf1  20001  dmdprdsplit2lem  20013  dmdprdsplit2  20014  ablfaclem3  20055  prdsmgp  20123  unitgrp  20354  subdrgint  20775  crng2idl  21274  gsumfsum  21409  pzriprnglem6  21461  chrid  21500  znleval  21529  frgpcyg  21548  ofldchr  21551  ocv1  21654  frlmip  21753  ellspd  21777  psrass1lem  21908  evlsvvval  22069  selvvvval  22118  ply1chr  22292  evl1var  22322  pf1mpf  22338  pf1ind  22341  mamuvs2  22389  madurid  22627  baspartn  22937  mretopd  23075  ordtcld1  23180  ordtcld2  23181  leordtvallem1  23193  leordtvallem2  23194  paste  23277  imacmp  23380  cmpsub  23383  unconn  23412  1stckgen  23537  ptbasfi  23564  txcld  23586  ptclsg  23598  txdis1cn  23618  ptrescn  23622  hausdiag  23628  txkgen  23635  xkoptsub  23637  xkococnlem  23642  cnmpt21  23654  cnmpt22  23657  tgqtop  23695  qtoprest  23700  kqdisj  23715  hmeores  23754  hmphindis  23780  pt1hmeo  23789  ptuncnv  23790  ptunhmeo  23791  xpstopnlem1  23792  xkohmeo  23798  alexsublem  24027  ptcmplem2  24036  tmdcn2  24072  cldsubg  24094  qustgplem  24104  tsmsres  24127  ustbas2  24208  ressuss  24245  metreslem  24345  xpsdsval  24364  prdsxmslem2  24512  txmetcnp  24530  tngngp  24637  nrmtngdist  24640  remetdval  24772  cnheibor  24940  evth2  24945  pcoass  25009  ncvspi  25141  iscmet3  25278  rrxip  25375  minveclem2  25411  cmmbl  25519  nulmbl2  25521  volinun  25531  voliunlem1  25535  volsup  25541  ovolioo  25553  uniiccdif  25563  uniioombllem2  25568  uniioombllem3  25570  uniioombllem4  25571  uniioombllem5  25572  ismbf3d  25639  itg2uba  25728  itg2i1fseq  25740  itgsplitioo  25823  limcflf  25866  cnplimc  25872  limcun  25880  dvfval  25882  dvres  25896  dvres3a  25899  dvnp1  25910  dvn1  25911  dvexp3  25963  dvsincos  25966  mvth  25977  c1lip2  25983  dvfsumlem2  26012  itgsubstlem  26033  itgsubst  26034  coeeq2  26225  dgreq0  26248  dgrcolem2  26257  vieta1  26296  ulm2  26368  radcnv0  26399  abelthlem2  26415  tanarg  26601  advlogexp  26637  efopn  26640  logtayl  26642  cxpcn3  26730  ang180lem3  26793  quad2  26821  mcubic  26829  binom4  26832  dquart  26835  quart1lem  26837  quart1  26838  quartlem1  26839  asinlem3a  26852  efiatan  26894  tanatan  26901  atanbndlem  26907  dvatan  26917  wilthlem2  27050  ftalem3  27056  ftalem5  27058  basellem3  27064  mumullem2  27161  musum  27172  mpodvdsmulf1o  27175  chtublem  27192  perfectlem2  27211  bposlem6  27270  bposlem9  27273  1lgs  27321  lgs1  27322  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgsquadlem2  27362  lgsquad2lem2  27366  2sqblem  27412  rpvmasum2  27493  log2sumbnd  27525  noetasuplem4  27718  ltslpss  27918  leslss  27919  bdayfinbndlem1  28477  z12shalf  28490  opphllem3  28835  vtxdun  29568  clwwlknon2num  30193  eucrct2eupth  30333  ex-fpar  30550  nvpi  30756  nvop  30765  phop  30907  minvecolem2  30964  hi01  31185  pjchi  31521  chjidm  31609  mayete3i  31817  ho0val  31839  lnop0  32055  adjbdlnb  32173  pjin2i  32282  mdslmd3i  32421  mdexchi  32424  imadifxp  32690  fcoinver  32693  suppovss  32773  fressupp  32780  supppreima  32783  mptprop  32790  f1od2  32811  fcobijfs  32813  ffsrn  32820  iocinif  32873  difioo  32874  indf1ofs  32945  s2rnOLD  33023  s3rnOLD  33025  cshw1s2  33039  gsummpt2co  33129  gsumhashmul  33148  gsummulsubdishift1s  33151  gsummulsubdishift2s  33152  symgfcoeu  33163  symgcom  33164  pmtrprfv2  33169  pmtrcnel2  33171  tocyc01  33199  cycpmconjv  33223  cycpmconjs  33237  elrgspnlem2  33324  lsmsnorb2  33475  krull  33562  opprqusbas  33571  opprqusplusg  33572  qsdrngi  33578  psrgsum  33732  psrmonprod  33736  ply1degltdimlem  33806  lindsun  33809  dimkerim  33811  fldexttr  33842  constrcon  33958  cos9thpiminplylem3  33968  smatlem  33981  zarcmplem  34065  esumpad2  34240  hasheuni  34269  esumcvg2  34271  esum2dlem  34276  sigapildsys  34346  measxun2  34394  measunl  34400  measinblem  34404  carsgclctunlem1  34501  carsgclctunlem3  34504  sibfof  34524  sitgclg  34526  eulerpartlemgf  34563  probdif  34604  cndprobval  34617  ballotlemic  34691  signsvtn0  34754  signstres  34759  chtvalz  34813  hgt750lemd  34832  bnj1415  35220  f1resrcmplf1d  35268  f1resfz0f1d  35342  revwlk  35353  subfacp1lem1  35407  subfacp1lem3  35410  subfacp1lem5  35412  cvmscld  35501  cvmlift2lem9a  35531  cvmlift2lem9  35539  fwddifnp1  36393  dfttc4  36758  finxpreclem5  37757  ptrest  37986  poimirlem2  37989  poimirlem3  37990  poimirlem6  37993  poimirlem7  37994  poimirlem9  37996  poimirlem11  37998  poimirlem12  37999  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem24  38011  poimirlem25  38012  poimirlem27  38014  poimirlem28  38015  poimirlem29  38016  poimirlem31  38018  voliunnfl  38031  volsupnfl  38032  mbfresfi  38033  itg2addnclem2  38039  itg2addnclem3  38040  ftc1anclem5  38064  dvacos  38072  areacirclem5  38079  cocnv  38092  istotbnd3  38138  ssbnd  38155  disjresdisj  38611  eccnvepres3  38659  dfblockliftmap2  38828  symrelim  39010  osumcllem9N  40456  4atexlemex2  40563  cdleme20j  40810  cdlemg47  41228  diaintclN  41550  dibintclN  41659  dihintcl  41836  lclkrlem2e  42003  lclkrlem2p  42014  lcfrlem31  42065  lcmineqlem  42537  sticksstones8  42638  dvun  42836  readdlid  42880  fsuppssind  43043  prjspnval2  43068  flt4lem  43095  diophin  43221  monotuz  43386  monotoddzzfi  43387  oddcomabszz  43389  fnwe2val  43494  lnmlmic  43533  fiuneneq  43637  cytpval  43647  oaun3  43827  ntrkbimka  44482  ntrneifv2  44524  mnringmulrd  44667  mnringmulrcld  44672  radcnvrat  44758  nzprmdif  44763  binomcxplemnotnn0  44800  ioccncflimc  46328  icocncflimc  46332  stoweidlem50  46493  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem107  46656  lambert0  47350  lamberte  47351  elsprel  47950  reuopreuprim  48001  perfectALTVlem2  48213  dfnbgr6  48348  dfsclnbgr6  48349  restclssep  49406  seposep  49416  iscnrm3rlem8  49437  swapfid  49769  cofuswapf1  49784  cofuswapf2  49785  idfudiag1lem  50013  termcfuncval  50022  ranval  50110  lmddu  50157  initocmd  50159  logb2aval  50254  aacllem  50291