Theorem eqtr3id 2818

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  3eqtr3g  2827  csbeq1a  3875  ssdifeq0  4452  pofun  5588  opabbi2dv  5836  cnvsng  6225  csbpredg  6309  funcnvpr  6599  funcnvtp  6600  funcnvqp  6601  fresin  6748  fresaunres2  6751  f1imacnv  6838  foimacnv  6839  funfv  6969  dffv2  6977  fimacnvinrn  7067  rescnvimafod  7069  fsn2  7133  funiunfvf  7248  fcof1oinvd  7292  riotaxfrd  7402  f1opw2  7666  fnexALT  7947  fparlem3  8108  fparlem4  8109  fsplitfpar  8112  fvproj  8129  mpocurryd  8264  seqomlem1  8436  seqomlem4  8439  oasuc  8508  oesuclem  8509  omsuc  8510  onasuc  8512  onmsuc  8513  eqerlem  8729  pmresg  8867  fopwdom  9072  sbthlem8  9081  sbthlem9  9082  fodomr  9115  domss2  9123  mapen  9128  cnvfi  9159  fiint  9285  fodomfir  9286  f1opwfi  9312  mapfien  9367  marypha1lem  9392  unxpwdom  9550  cantnfval2  9637  ttrcltr  9684  infxpenlem  9996  djuinf  10171  isf34lem3  10358  isf34lem5  10361  axdc4lem  10438  ttukeylem6  10497  rankcf  10761  tskuni  10767  gruima  10786  dmrecnq  10952  ltexnq  10959  reclem3pr  11033  pn0sr  11085  mulgt0sr  11089  recdiv  11920  2resupmax  13213  max0sub  13221  rexmul  13296  xmulmnf1  13301  xmulm1  13306  prunioo  13507  fseq1p1m1  13625  fzshftral  13642  seqp1d  14053  seqf1olem2  14077  seqfeq4  14086  binom3  14259  expmulnbnd  14270  discr  14275  bcn2  14354  hashun2  14418  hashun3  14419  hashdif  14449  hashgt12el  14458  hashgt12el2  14459  hashfacen  14490  s2prop  14943  s4prop  14946  s3sndisj  15003  s3iunsndisj  15004  cnrecnv  15215  rddif  15391  amgm2  15420  rlimres  15608  lo1res  15609  iseraltlem2  15733  iseralt  15735  fsumss  15775  fsumcl2lem  15781  isumclim3  15809  fsumcnv  15823  telfsumo  15853  fsumiun  15872  arisum2  15914  geoisum1c  15933  fprodss  16001  fprodser  16002  fprodcl2lem  16003  fprodsplit  16019  fprodn0  16032  fprodcnv  16036  iprodclim3  16053  risefac1  16086  fallfac1  16087  bpolyval  16102  bpoly3  16111  bpoly4  16112  fsumcube  16113  sinhval  16209  cos01bnd  16241  ruclem6  16290  sadadd2lem2  16507  eucalgval  16639  pcid  16932  prmreclem4  16978  4sqlem15  17018  4sqlem16  17019  ramcl  17088  strfv2d  17260  setsid  17266  imasvscafn  17590  xpsff1o  17620  xpsaddlem  17626  xpsvsca  17630  xpsle  17632  mreexexlem2d  17700  mreexexlem4d  17702  sscres  17879  xpcid  18244  evlfcllem  18276  hofcl  18314  isacs5lem  18600  frmdup3lem  18924  cayleylem2  19482  f1omvdco2  19517  symggen  19539  psgnunilem1  19562  pgp0  19665  sylow3lem2  19697  lsmdisjr  19753  lsmdisj2r  19754  subgdisj2  19761  efgval  19786  frgpuplem  19841  frgpup2  19845  gsumval3  19976  gsumzres  19978  gsum2d2lem  20042  dprdf1  20104  dmdprdsplit2lem  20116  dmdprdsplit2  20117  ablfaclem3  20158  prdsmgp  20226  unitgrp  20464  subdrgint  20883  crng2idl  21390  gsumfsum  21552  pzriprnglem6  21604  chrid  21643  znleval  21672  frgpcyg  21691  ofldchr  21694  ocv1  21797  frlmip  21896  ellspd  21920  psrass1lem  22051  evlsvvval  22212  selvvvval  22261  ply1chr  22434  evl1var  22464  pf1mpf  22480  pf1ind  22483  mamuvs2  22531  madurid  22769  baspartn  23079  mretopd  23217  ordtcld1  23322  ordtcld2  23323  leordtvallem1  23335  leordtvallem2  23336  paste  23419  imacmp  23522  cmpsub  23525  unconn  23554  1stckgen  23679  ptbasfi  23706  txcld  23728  ptclsg  23740  txdis1cn  23760  ptrescn  23764  hausdiag  23770  txkgen  23777  xkoptsub  23779  xkococnlem  23784  cnmpt21  23796  cnmpt22  23799  tgqtop  23837  qtoprest  23842  kqdisj  23857  hmeores  23896  hmphindis  23922  pt1hmeo  23931  ptuncnv  23932  ptunhmeo  23933  xpstopnlem1  23934  xkohmeo  23940  alexsublem  24169  ptcmplem2  24178  tmdcn2  24214  cldsubg  24236  qustgplem  24246  tsmsres  24269  ustbas2  24350  ressuss  24387  metreslem  24487  xpsdsval  24506  prdsxmslem2  24654  txmetcnp  24672  tngngp  24779  nrmtngdist  24782  remetdval  24914  cnheibor  25082  evth2  25087  pcoass  25151  ncvspi  25283  iscmet3  25420  rrxip  25517  minveclem2  25553  cmmbl  25661  nulmbl2  25663  volinun  25673  voliunlem1  25677  volsup  25683  ovolioo  25695  uniiccdif  25705  uniioombllem2  25710  uniioombllem3  25712  uniioombllem4  25713  uniioombllem5  25714  ismbf3d  25781  itg2uba  25870  itg2i1fseq  25882  itgsplitioo  25965  limcflf  26008  cnplimc  26014  limcun  26022  dvfval  26024  dvres  26038  dvres3a  26041  dvnp1  26052  dvn1  26053  dvexp3  26105  dvsincos  26108  mvth  26119  c1lip2  26125  dvfsumlem2  26154  itgsubstlem  26175  itgsubst  26176  coeeq2  26367  dgreq0  26390  dgrcolem2  26399  vieta1  26441  ulm2  26513  radcnv0  26544  abelthlem2  26560  tanarg  26749  advlogexp  26785  efopn  26788  logtayl  26790  cxpcn3  26878  ang180lem3  26941  quad2  26969  mcubic  26977  binom4  26980  dquart  26983  quart1lem  26985  quart1  26986  quartlem1  26987  asinlem3a  27000  efiatan  27042  tanatan  27049  atanbndlem  27055  dvatan  27065  wilthlem2  27198  ftalem3  27204  ftalem5  27206  basellem3  27212  mumullem2  27309  musum  27320  mpodvdsmulf1o  27323  chtublem  27340  perfectlem2  27359  bposlem6  27418  bposlem9  27421  1lgs  27469  lgs1  27470  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem3  27506  lgsquadlem2  27510  lgsquad2lem2  27514  2sqblem  27560  rpvmasum2  27641  log2sumbnd  27673  noetasuplem4  27865  ltslpss  28066  leslss  28067  bdayfinbndlem1  28625  z12shalf  28638  opphllem3  28988  prlngpln3  29151  vtxdun  29771  clwwlknon2num  30396  eucrct2eupth  30536  ex-fpar  30753  nvpi  30959  nvop  30968  phop  31110  minvecolem2  31167  hi01  31388  pjchi  31724  chjidm  31812  mayete3i  32020  ho0val  32042  lnop0  32258  adjbdlnb  32376  pjin2i  32485  mdslmd3i  32624  mdexchi  32627  imadifxp  32886  fcoinver  32889  suppovss  32966  fressupp  32973  supppreima  32976  mptprop  32983  f1od2  33004  fcobijfs  33006  ffsrn  33013  iocinif  33066  difioo  33067  indf1ofs  33126  s2rnOLD  33204  s3rnOLD  33206  cshw1s2  33220  gsummpt2co  33308  gsumhashmul  33327  gsummulsubdishift1s  33330  gsummulsubdishift2s  33331  symgfcoeu  33342  symgcom  33343  pmtrprfv2  33348  pmtrcnel2  33350  tocyc01  33378  cycpmconjv  33402  cycpmconjs  33416  elrgspnlem2  33503  lsmsnorb2  33648  krull  33705  opprqusbas  33714  opprqusplusg  33715  qsdrngi  33721  psrgsum  33882  psrmonprod  33886  ply1degltdimlem  33956  lindsun  33959  dimkerim  33961  fldexttr  33992  constrcon  34108  cos9thpiminplylem3  34118  smatlem  34131  zarcmplem  34215  esumpad2  34390  hasheuni  34419  esumcvg2  34421  esum2dlem  34426  sigapildsys  34496  measxun2  34544  measunl  34550  measinblem  34554  carsgclctunlem1  34651  carsgclctunlem3  34654  sibfof  34674  sitgclg  34676  eulerpartlemgf  34713  probdif  34754  cndprobval  34767  ballotlemic  34841  signsvtn0  34901  signstres  34906  chtvalz  34960  hgt750lemd  34979  bnj1415  35370  f1resrcmplf1d  35418  f1resfz0f1d  35503  revwlk  35515  subfacp1lem1  35569  subfacp1lem3  35572  subfacp1lem5  35574  cvmscld  35663  cvmlift2lem9a  35693  cvmlift2lem9  35701  fwddifnp1  36555  dfttc4  36929  finxpreclem5  37928  ptrest  38157  poimirlem2  38160  poimirlem3  38161  poimirlem6  38164  poimirlem7  38165  poimirlem9  38167  poimirlem11  38169  poimirlem12  38170  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem24  38182  poimirlem25  38183  poimirlem27  38185  poimirlem28  38186  poimirlem29  38187  poimirlem31  38189  voliunnfl  38202  volsupnfl  38203  mbfresfi  38204  itg2addnclem2  38210  itg2addnclem3  38211  ftc1anclem5  38235  dvacos  38243  areacirclem5  38250  cocnv  38263  istotbnd3  38309  ssbnd  38326  disjresdisj  38782  eccnvepres3  38830  dfblockliftmap2  38999  symrelim  39181  osumcllem9N  40627  4atexlemex2  40734  cdleme20j  40981  cdlemg47  41399  diaintclN  41721  dibintclN  41830  dihintcl  42007  lclkrlem2e  42174  lclkrlem2p  42185  lcfrlem31  42236  lcmineqlem  42708  sticksstones8  42809  dvun  43009  readdlid  43053  fsuppssind  43216  prjspnval2  43241  flt4lem  43268  diophin  43394  monotuz  43559  monotoddzzfi  43560  oddcomabszz  43562  fnwe2val  43667  lnmlmic  43706  fiuneneq  43810  cytpval  43820  oaun3  44000  ntrkbimka  44655  ntrneifv2  44697  mnringmulrd  44838  mnringmulrcld  44843  radcnvrat  44915  nzprmdif  44920  binomcxplemnotnn0  44957  limsupvaluz  46313  ioccncflimc  46490  icocncflimc  46494  stoweidlem50  46655  fourierdlem48  46759  fourierdlem49  46760  fourierdlem89  46800  fourierdlem90  46801  fourierdlem91  46802  fourierdlem107  46818  lambert0  47512  lamberte  47513  elsprel  48112  reuopreuprim  48163  perfectALTVlem2  48375  dfnbgr6  48510  dfsclnbgr6  48511  smprngprmrng  48992  restclssep  49578  seposep  49588  iscnrm3rlem8  49609  swapfid  49941  cofuswapf1  49956  cofuswapf2  49957  idfudiag1lem  50185  termcfuncval  50194  ranval  50282  lmddu  50329  initocmd  50331  logb2aval  50426  aacllem  50474