Theorem eqtr3id 2814

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  3eqtr3g  2823  csbeq1a  3868  ssdifeq0  4449  pofun  5589  opabbi2dv  5837  cnvsng  6226  csbpredg  6312  funcnvpr  6602  funcnvtp  6603  funcnvqp  6604  fresin  6751  fresaunres2  6754  f1imacnv  6841  foimacnv  6842  funfv  6972  dffv2  6980  fimacnvinrn  7070  rescnvimafod  7072  fsn2  7136  funiunfvf  7252  f1resrcmplf1d  7278  fcof1oinvd  7300  riotaxfrd  7410  f1opw2  7675  fnexALT  7954  fparlem3  8115  fparlem4  8116  fsplitfpar  8119  fvproj  8136  mpocurryd  8271  seqomlem1  8443  seqomlem4  8446  oasuc  8515  oesuclem  8516  omsuc  8517  onasuc  8519  onmsuc  8520  eqerlem  8736  pmresg  8874  fopwdom  9080  sbthlem8  9089  sbthlem9  9090  fodomr  9123  domss2  9131  mapen  9136  cnvfi  9167  fiint  9293  fodomfir  9294  f1opwfi  9320  mapfien  9375  marypha1lem  9400  unxpwdom  9558  cantnfval2  9645  ttrcltr  9692  infxpenlem  10013  djuinf  10188  isf34lem3  10374  isf34lem5  10377  axdc4lem  10454  ttukeylem6  10513  rankcf  10777  tskuni  10783  gruima  10802  dmrecnq  10968  ltexnq  10975  reclem3pr  11049  pn0sr  11101  mulgt0sr  11105  recdiv  11936  2resupmax  13230  max0sub  13238  rexmul  13313  xmulmnf1  13318  xmulm1  13323  prunioo  13524  fseq1p1m1  13643  fzshftral  13660  f1resfz0f1d  13838  seqp1d  14072  seqf1olem2  14096  seqfeq4  14105  binom3  14278  expmulnbnd  14289  discr  14294  bcn2  14373  hashun2  14437  hashun3  14438  hashdif  14468  hashgt12el  14477  hashgt12el2  14478  hashfacen  14509  s2prop  14968  s4prop  14971  s3sndisj  15028  s3iunsndisj  15029  cnrecnv  15240  rddif  15416  amgm2  15445  rlimres  15633  lo1res  15634  iseraltlem2  15758  iseralt  15760  fsumss  15799  fsumcl2lem  15805  isumclim3  15833  fsumcnv  15847  telfsumo  15877  fsumiun  15896  arisum2  15938  geoisum1c  15957  fprodss  16025  fprodser  16026  fprodcl2lem  16027  fprodsplit  16043  fprodn0  16056  fprodcnv  16060  iprodclim3  16077  risefac1  16109  fallfac1  16110  bpolyval  16125  bpoly3  16134  bpoly4  16135  fsumcube  16136  sinhval  16232  cos01bnd  16264  ruclem6  16313  sadadd2lem2  16530  eucalgval  16662  pcid  16955  prmreclem4  17001  4sqlem15  17041  4sqlem16  17042  ramcl  17111  strfv2d  17283  setsid  17289  imasvscafn  17613  xpsff1o  17643  xpsaddlem  17649  xpsvsca  17653  xpsle  17655  mreexexlem2d  17723  mreexexlem4d  17725  sscres  17902  xpcid  18267  evlfcllem  18299  hofcl  18337  isacs5lem  18623  frmdup3lem  18962  cayleylem2  19527  f1omvdco2  19562  symggen  19584  psgnunilem1  19607  pgp0  19710  sylow3lem2  19742  lsmdisjr  19798  lsmdisj2r  19799  subgdisj2  19806  efgval  19831  frgpuplem  19886  frgpup2  19890  gsumval3  20021  gsumzres  20023  gsum2d2lem  20087  dprdf1  20149  dmdprdsplit2lem  20161  dmdprdsplit2  20162  ablfaclem3  20203  prdsmgp  20271  unitgrp  20511  subdrgint  20956  crng2idl  21470  gsumfsum  21634  pzriprnglem6  21686  chrid  21725  znleval  21754  frgpcyg  21773  ofldchr  21776  ocv1  21879  frlmip  21978  ellspd  22002  psrass1lem  22133  evlsvvval  22294  selvvvval  22343  ply1chr  22516  evl1var  22546  pf1mpf  22562  pf1ind  22565  mamuvs2  22613  madurid  22851  baspartn  23161  mretopd  23299  ordtcld1  23404  ordtcld2  23405  leordtvallem1  23417  leordtvallem2  23418  paste  23501  imacmp  23604  cmpsub  23607  unconn  23636  1stckgen  23762  ptbasfi  23789  txcld  23811  ptclsg  23823  txdis1cn  23843  ptrescn  23847  hausdiag  23853  txkgen  23860  xkoptsub  23862  xkococnlem  23867  cnmpt21  23879  cnmpt22  23882  tgqtop  23920  qtoprest  23925  kqdisj  23940  hmeores  23979  hmphindis  24005  pt1hmeo  24014  ptuncnv  24015  ptunhmeo  24016  xpstopnlem1  24017  xkohmeo  24023  alexsublem  24252  ptcmplem2  24261  tmdcn2  24297  cldsubg  24319  qustgplem  24329  tsmsres  24352  ustbas2  24433  ressuss  24470  metreslem  24570  xpsdsval  24589  prdsxmslem2  24737  txmetcnp  24755  tngngp  24862  nrmtngdist  24865  remetdval  24997  cnheibor  25165  evth2  25170  pcoass  25234  ncvspi  25366  iscmet3  25503  rrxip  25600  minveclem2  25636  cmmbl  25744  nulmbl2  25746  volinun  25756  voliunlem1  25760  volsup  25766  ovolioo  25778  uniiccdif  25788  uniioombllem2  25793  uniioombllem3  25795  uniioombllem4  25796  uniioombllem5  25797  ismbf3d  25864  itg2uba  25953  itg2i1fseq  25965  itgsplitioo  26048  limcflf  26091  cnplimc  26097  limcun  26105  dvfval  26107  dvres  26121  dvres3a  26124  dvnp1  26135  dvn1  26136  dvexp3  26188  dvsincos  26191  mvth  26202  c1lip2  26208  dvfsumlem2  26237  itgsubstlem  26258  itgsubst  26259  coeeq2  26450  dgreq0  26473  dgrcolem2  26482  vieta1  26524  ulm2  26599  radcnv0  26630  abelthlem2  26646  tanarg  26835  advlogexp  26871  efopn  26874  logtayl  26876  cxpcn3  26964  ang180lem3  27027  quad2  27055  mcubic  27063  binom4  27066  dquart  27069  quart1lem  27071  quart1  27072  quartlem1  27073  asinlem3a  27086  efiatan  27128  tanatan  27135  atanbndlem  27141  dvatan  27151  wilthlem2  27284  ftalem3  27290  ftalem5  27292  basellem3  27298  mumullem2  27395  musum  27406  mpodvdsmulf1o  27409  ppiub  27419  chtublem  27426  perfectlem2  27445  bposlem6  27504  bposlem9  27507  1lgs  27555  lgs1  27556  lgseisenlem1  27590  lgseisenlem2  27591  lgseisenlem3  27592  lgsquadlem2  27596  lgsquad2lem2  27600  2sqblem  27646  rpvmasum2  27727  log2sumbnd  27759  noetasuplem4  27951  ltslpss  28152  leslss  28153  bdayfinbndlem1  28711  z12shalf  28724  opphllem3  29081  prlngpln3  29254  vtxdun  29889  revwlk  30094  clwwlknon2num  30523  eucrct2eupth  30667  ex-fpar  30884  nvpi  31090  nvop  31099  phop  31241  minvecolem2  31298  hi01  31519  pjchi  31855  chjidm  31943  mayete3i  32151  ho0val  32173  lnop0  32389  adjbdlnb  32507  pjin2i  32616  mdslmd3i  32755  mdexchi  32758  imadifxp  33017  fcoinver  33020  suppovss  33097  fressupp  33104  supppreima  33107  mptprop  33114  f1od2  33134  fcobijfs  33136  ffsrn  33143  iocinif  33196  difioo  33197  indf1ofs  33256  cshw1s2  33344  gsummpt2co  33432  gsumhashmul  33451  gsummulsubdishift1s  33454  gsummulsubdishift2s  33455  symgfcoeu  33466  symgcom  33467  pmtrprfv2  33472  pmtrcnel2  33474  tocyc01  33502  cycpmconjv  33526  cycpmconjs  33540  elrgspnlem2  33627  lsmsnorb2  33769  krull  33825  opprqusbas  33834  opprqusplusg  33835  qsdrngi  33841  psrgsum  34002  psrmonprod  34006  ply1degltdimlem  34076  lindsun  34079  dimkerim  34081  fldexttr  34112  constrcon  34228  cos9thpiminplylem3  34238  smatlem  34251  zarcmplem  34335  esumpad2  34510  hasheuni  34539  esumcvg2  34541  esum2dlem  34546  sigapildsys  34617  measxun2  34665  measunl  34671  measinblem  34675  carsgclctunlem1  34772  carsgclctunlem3  34775  sibfof  34795  sitgclg  34797  eulerpartlemgf  34834  probdif  34875  cndprobval  34888  ballotlemic  34962  signsvtn0  35022  signstres  35027  chtvalz  35081  hgt750lemd  35100  bnj1415  35491  subfacp1lem1  35708  subfacp1lem3  35711  subfacp1lem5  35713  cvmscld  35802  cvmlift2lem9a  35832  cvmlift2lem9  35840  fwddifnp1  36694  dfttc4  37098  finxpreclem5  38098  ptrest  38327  poimirlem2  38330  poimirlem3  38331  poimirlem6  38334  poimirlem7  38335  poimirlem9  38337  poimirlem11  38339  poimirlem12  38340  poimirlem16  38344  poimirlem17  38345  poimirlem19  38347  poimirlem20  38348  poimirlem24  38352  poimirlem25  38353  poimirlem27  38355  poimirlem28  38356  poimirlem29  38357  poimirlem31  38359  voliunnfl  38372  volsupnfl  38373  mbfresfi  38374  itg2addnclem2  38380  itg2addnclem3  38381  ftc1anclem5  38405  dvacos  38413  areacirclem5  38420  cocnv  38434  istotbnd3  38480  ssbnd  38497  disjresdisj  38951  eccnvepres3  38999  dfblockliftmap2  39168  symrelim  39350  osumcllem9N  40796  4atexlemex2  40903  cdleme20j  41150  cdlemg47  41568  diaintclN  41890  dibintclN  41999  dihintcl  42176  lclkrlem2e  42343  lclkrlem2p  42354  lcfrlem31  42405  lcmineqlem  42877  sticksstones8  42978  dvun  43178  readdlid  43222  fsuppssind  43383  prjspnval2  43408  flt4lem  43435  diophin  43561  monotuz  43726  monotoddzzfi  43727  oddcomabszz  43729  fnwe2val  43834  lnmlmic  43873  fiuneneq  43977  cytpval  43987  oaun3  44167  ntrkbimka  44822  ntrneifv2  44864  mnringmulrd  45005  mnringmulrcld  45010  radcnvrat  45082  nzprmdif  45087  binomcxplemnotnn0  45124  limsupvaluz  46480  ioccncflimc  46657  icocncflimc  46661  stoweidlem50  46822  fourierdlem48  46926  fourierdlem49  46927  fourierdlem89  46967  fourierdlem90  46968  fourierdlem91  46969  fourierdlem107  46985  lambert0  47682  lamberte  47683  elsprel  48282  reuopreuprim  48333  perfectALTVlem2  48545  dfnbgr6  48680  dfsclnbgr6  48681  smprngprmrng  49161  restclssep  49751  seposep  49761  iscnrm3rlem8  49782  swapfid  50114  cofuswapf1  50129  cofuswapf2  50130  idfudiag1lem  50358  termcfuncval  50367  ranval  50455  lmddu  50502  initocmd  50504  logb2aval  50599  aacllem  50678