Theorem eqtr3id 2782

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 2780	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  3eqtr3g  2791  csbeq1a  3860  ssdifeq0  4436  pofun  5547  opabbi2dv  5795  cnvsng  6178  csbpredg  6262  funcnvpr  6551  funcnvtp  6552  funcnvqp  6553  f1imadifssran  6575  fresin  6700  fresaunres2  6703  f1imacnv  6787  foimacnv  6788  funfv  6918  dffv2  6926  fimacnvinrn  7013  rescnvimafod  7015  fsn2  7078  funiunfvf  7192  fcof1oinvd  7236  riotaxfrd  7346  f1opw2  7610  fnexALT  7892  fparlem3  8053  fparlem4  8054  fsplitfpar  8057  fvproj  8073  mpocurryd  8208  seqomlem1  8378  seqomlem4  8381  oasuc  8448  oesuclem  8449  omsuc  8450  onasuc  8452  onmsuc  8453  eqerlem  8666  pmresg  8804  fopwdom  9009  sbthlem8  9018  sbthlem9  9019  fodomr  9052  domss2  9060  mapen  9065  cnvfi  9096  fiint  9222  fodomfir  9223  f1opwfi  9251  mapfien  9303  marypha1lem  9328  unxpwdom  9486  cantnfval2  9570  ttrcltr  9617  infxpenlem  9915  djuinf  10091  isf34lem3  10277  isf34lem5  10280  axdc4lem  10357  ttukeylem6  10416  rankcf  10679  tskuni  10685  gruima  10704  dmrecnq  10870  ltexnq  10877  reclem3pr  10951  pn0sr  11003  mulgt0sr  11007  recdiv  11838  2resupmax  13094  max0sub  13102  rexmul  13177  xmulmnf1  13182  xmulm1  13187  prunioo  13388  fseq1p1m1  13505  fzshftral  13522  seqp1d  13932  seqf1olem2  13956  seqfeq4  13965  binom3  14138  expmulnbnd  14149  discr  14154  bcn2  14233  hashun2  14297  hashun3  14298  hashdif  14327  hashgt12el  14336  hashgt12el2  14337  hashfacen  14368  s2prop  14821  s4prop  14824  s3sndisj  14881  s3iunsndisj  14882  cnrecnv  15079  rddif  15255  amgm2  15284  rlimres  15472  lo1res  15473  iseraltlem2  15597  iseralt  15599  fsumss  15639  fsumcl2lem  15645  isumclim3  15673  fsumcnv  15687  telfsumo  15716  fsumiun  15735  arisum2  15775  geoisum1c  15794  fprodss  15862  fprodser  15863  fprodcl2lem  15864  fprodsplit  15880  fprodn0  15893  fprodcnv  15897  iprodclim3  15914  risefac1  15947  fallfac1  15948  bpolyval  15963  bpoly3  15972  bpoly4  15973  fsumcube  15974  sinhval  16070  cos01bnd  16102  ruclem6  16151  sadadd2lem2  16368  eucalgval  16500  pcid  16792  prmreclem4  16838  4sqlem15  16878  4sqlem16  16879  ramcl  16948  strfv2d  17119  setsid  17125  imasvscafn  17449  xpsff1o  17479  xpsaddlem  17485  xpsvsca  17489  xpsle  17491  mreexexlem2d  17559  mreexexlem4d  17561  sscres  17738  xpcid  18103  evlfcllem  18135  hofcl  18173  isacs5lem  18459  frmdup3lem  18782  cayleylem2  19333  f1omvdco2  19368  symggen  19390  psgnunilem1  19413  pgp0  19516  sylow3lem2  19548  lsmdisjr  19604  lsmdisj2r  19605  subgdisj2  19612  efgval  19637  frgpuplem  19692  frgpup2  19696  gsumval3  19827  gsumzres  19829  gsum2d2lem  19893  dprdf1  19955  dmdprdsplit2lem  19967  dmdprdsplit2  19968  ablfaclem3  20009  prdsmgp  20077  unitgrp  20310  subdrgint  20727  crng2idl  21227  gsumfsum  21380  pzriprnglem6  21432  chrid  21471  znleval  21500  frgpcyg  21519  ofldchr  21522  ocv1  21625  frlmip  21724  ellspd  21748  psrass1lem  21879  evlsvvval  22039  ply1chr  22241  evl1var  22271  pf1mpf  22287  pf1ind  22290  mamuvs2  22341  madurid  22579  baspartn  22889  mretopd  23027  ordtcld1  23132  ordtcld2  23133  leordtvallem1  23145  leordtvallem2  23146  paste  23229  imacmp  23332  cmpsub  23335  unconn  23364  1stckgen  23489  ptbasfi  23516  txcld  23538  ptclsg  23550  txdis1cn  23570  ptrescn  23574  hausdiag  23580  txkgen  23587  xkoptsub  23589  xkococnlem  23594  cnmpt21  23606  cnmpt22  23609  tgqtop  23647  qtoprest  23652  kqdisj  23667  hmeores  23706  hmphindis  23732  pt1hmeo  23741  ptuncnv  23742  ptunhmeo  23743  xpstopnlem1  23744  xkohmeo  23750  alexsublem  23979  ptcmplem2  23988  tmdcn2  24024  cldsubg  24046  qustgplem  24056  tsmsres  24079  ustbas2  24160  ressuss  24197  metreslem  24297  xpsdsval  24316  prdsxmslem2  24464  txmetcnp  24482  tngngp  24589  nrmtngdist  24592  remetdval  24724  cnheibor  24901  evth2  24906  pcoass  24971  ncvspi  25103  iscmet3  25240  rrxip  25337  minveclem2  25373  cmmbl  25482  nulmbl2  25484  volinun  25494  voliunlem1  25498  volsup  25504  ovolioo  25516  uniiccdif  25526  uniioombllem2  25531  uniioombllem3  25533  uniioombllem4  25534  uniioombllem5  25535  ismbf3d  25602  itg2uba  25691  itg2i1fseq  25703  itgsplitioo  25786  limcflf  25829  cnplimc  25835  limcun  25843  dvfval  25845  dvres  25859  dvres3a  25862  dvnp1  25874  dvn1  25875  dvexp3  25929  dvsincos  25932  mvth  25944  c1lip2  25950  dvfsumlem2  25980  dvfsumlem2OLD  25981  itgsubstlem  26002  itgsubst  26003  coeeq2  26194  dgreq0  26218  dgrcolem2  26227  vieta1  26267  ulm2  26341  radcnv0  26372  abelthlem2  26389  tanarg  26575  advlogexp  26611  efopn  26614  logtayl  26616  cxpcn3  26705  ang180lem3  26768  quad2  26796  mcubic  26804  binom4  26807  dquart  26810  quart1lem  26812  quart1  26813  quartlem1  26814  asinlem3a  26827  efiatan  26869  tanatan  26876  atanbndlem  26882  dvatan  26892  wilthlem2  27026  ftalem3  27032  ftalem5  27034  basellem3  27040  mumullem2  27137  musum  27148  mpodvdsmulf1o  27151  chtublem  27169  perfectlem2  27188  bposlem6  27247  bposlem9  27250  1lgs  27298  lgs1  27299  lgseisenlem1  27333  lgseisenlem2  27334  lgseisenlem3  27335  lgsquadlem2  27339  lgsquad2lem2  27343  2sqblem  27389  rpvmasum2  27470  log2sumbnd  27502  noetasuplem4  27695  sltlpss  27873  slelss  27874  zs12half  28410  opphllem3  28747  vtxdun  29481  clwwlknon2num  30106  eucrct2eupth  30246  ex-fpar  30463  nvpi  30668  nvop  30677  phop  30819  minvecolem2  30876  hi01  31097  pjchi  31433  chjidm  31521  mayete3i  31729  ho0val  31751  lnop0  31967  adjbdlnb  32085  pjin2i  32194  mdslmd3i  32333  mdexchi  32336  imadifxp  32602  fcoinver  32605  suppovss  32686  fressupp  32693  supppreima  32696  mptprop  32703  padct  32725  f1od2  32726  fcobijfs  32728  ffsrn  32735  iocinif  32789  difioo  32790  indf1ofs  32876  s2rnOLD  32954  s3rnOLD  32956  cshw1s2  32970  gsummpt2co  33059  gsumhashmul  33078  gsummulsubdishift1s  33081  gsummulsubdishift2s  33082  symgfcoeu  33092  symgcom  33093  pmtrprfv2  33098  pmtrcnel2  33100  tocyc01  33128  cycpmconjv  33152  cycpmconjs  33166  elrgspnlem2  33253  lsmsnorb2  33401  krull  33488  opprqusbas  33497  opprqusplusg  33498  qsdrngi  33504  rgmoddimOLD  33695  ply1degltdimlem  33707  lindsun  33710  dimkerim  33712  fldexttr  33743  constrcon  33859  cos9thpiminplylem3  33869  smatlem  33882  zarcmplem  33966  esumpad2  34141  hasheuni  34170  esumcvg2  34172  esum2dlem  34177  sigapildsys  34247  measxun2  34295  measunl  34301  measinblem  34305  carsgclctunlem1  34402  carsgclctunlem3  34405  sibfof  34425  sitgclg  34427  eulerpartlemgf  34464  probdif  34505  cndprobval  34518  ballotlemic  34592  signsvtn0  34655  signstres  34660  chtvalz  34714  hgt750lemd  34733  bnj1415  35122  f1resrcmplf1d  35171  f1resfz0f1d  35230  revwlk  35241  subfacp1lem1  35295  subfacp1lem3  35298  subfacp1lem5  35300  cvmscld  35389  cvmlift2lem9a  35419  cvmlift2lem9  35427  fwddifnp1  36281  finxpreclem5  37512  ptrest  37732  poimirlem2  37735  poimirlem3  37736  poimirlem6  37739  poimirlem7  37740  poimirlem9  37742  poimirlem11  37744  poimirlem12  37745  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem24  37757  poimirlem25  37758  poimirlem27  37760  poimirlem28  37761  poimirlem29  37762  poimirlem31  37764  voliunnfl  37777  volsupnfl  37778  mbfresfi  37779  itg2addnclem2  37785  itg2addnclem3  37786  ftc1anclem5  37810  dvacos  37818  areacirclem5  37825  cocnv  37838  istotbnd3  37884  ssbnd  37901  disjresdisj  38352  eccnvepres3  38397  dfblockliftmap2  38547  symrelim  38728  osumcllem9N  40136  4atexlemex2  40243  cdleme20j  40490  cdlemg47  40908  diaintclN  41230  dibintclN  41339  dihintcl  41516  lclkrlem2e  41683  lclkrlem2p  41694  lcfrlem31  41745  lcmineqlem  42218  sticksstones8  42319  dvun  42529  readdlid  42573  selvvvval  42743  fsuppssind  42751  prjspnval2  42776  flt4lem  42803  diophin  42929  monotuz  43098  monotoddzzfi  43099  oddcomabszz  43101  fnwe2val  43206  lnmlmic  43245  fiuneneq  43349  cytpval  43359  oaun3  43539  ntrkbimka  44195  ntrneifv2  44237  mnringmulrd  44380  mnringmulrcld  44385  radcnvrat  44471  nzprmdif  44476  binomcxplemnotnn0  44513  ioccncflimc  46045  icocncflimc  46049  stoweidlem50  46210  fourierdlem89  46355  fourierdlem90  46356  fourierdlem91  46357  fourierdlem107  46373  lambert0  47049  lamberte  47050  elsprel  47637  reuopreuprim  47688  perfectALTVlem2  47884  dfnbgr6  48019  dfsclnbgr6  48020  restclssep  49077  seposep  49087  iscnrm3rlem8  49108  swapfid  49440  cofuswapf1  49455  cofuswapf2  49456  idfudiag1lem  49684  termcfuncval  49693  ranval  49781  lmddu  49828  initocmd  49830  logb2aval  49925  aacllem  49962