Theorem eqtr3id 2779

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  3eqtr3g  2788  csbeq1a  3879  ssdifeq0  4453  pofun  5567  opabbi2dv  5816  cnvsng  6199  csbpredg  6283  funcnvpr  6581  funcnvtp  6582  funcnvqp  6583  f1imadifssran  6605  fresin  6732  fresaunres2  6735  f1imacnv  6819  foimacnv  6820  funfv  6951  dffv2  6959  fimacnvinrn  7046  rescnvimafod  7048  fsn2  7111  funiunfvf  7226  fcof1oinvd  7271  riotaxfrd  7381  f1opw2  7647  fnexALT  7932  fparlem3  8096  fparlem4  8097  fsplitfpar  8100  fvproj  8116  mpocurryd  8251  seqomlem1  8421  seqomlem4  8424  oasuc  8491  oesuclem  8492  omsuc  8493  onasuc  8495  onmsuc  8496  eqerlem  8709  pmresg  8846  fopwdom  9054  sbthlem8  9064  sbthlem9  9065  fodomr  9098  domss2  9106  mapen  9111  cnvfi  9146  enp1iOLD  9232  xpfiOLD  9277  fiint  9284  fiintOLD  9285  fodomfir  9286  f1opwfi  9314  mapfien  9366  marypha1lem  9391  unxpwdom  9549  cantnfval2  9629  ttrcltr  9676  infxpenlem  9973  djuinf  10149  isf34lem3  10335  isf34lem5  10338  axdc4lem  10415  ttukeylem6  10474  rankcf  10737  tskuni  10743  gruima  10762  dmrecnq  10928  ltexnq  10935  reclem3pr  11009  pn0sr  11061  mulgt0sr  11065  recdiv  11895  2resupmax  13155  max0sub  13163  rexmul  13238  xmulmnf1  13243  xmulm1  13248  prunioo  13449  fseq1p1m1  13566  fzshftral  13583  seqp1d  13990  seqf1olem2  14014  seqfeq4  14023  binom3  14196  expmulnbnd  14207  discr  14212  bcn2  14291  hashun2  14355  hashun3  14356  hashdif  14385  hashgt12el  14394  hashgt12el2  14395  hashfacen  14426  s2prop  14880  s4prop  14883  s3sndisj  14940  s3iunsndisj  14941  cnrecnv  15138  rddif  15314  amgm2  15343  rlimres  15531  lo1res  15532  iseraltlem2  15656  iseralt  15658  fsumss  15698  fsumcl2lem  15704  isumclim3  15732  fsumcnv  15746  telfsumo  15775  fsumiun  15794  arisum2  15834  geoisum1c  15853  fprodss  15921  fprodser  15922  fprodcl2lem  15923  fprodsplit  15939  fprodn0  15952  fprodcnv  15956  iprodclim3  15973  risefac1  16006  fallfac1  16007  bpolyval  16022  bpoly3  16031  bpoly4  16032  fsumcube  16033  sinhval  16129  cos01bnd  16161  ruclem6  16210  sadadd2lem2  16427  eucalgval  16559  pcid  16851  prmreclem4  16897  4sqlem15  16937  4sqlem16  16938  ramcl  17007  strfv2d  17178  setsid  17184  imasvscafn  17507  xpsff1o  17537  xpsaddlem  17543  xpsvsca  17547  xpsle  17549  mreexexlem2d  17613  mreexexlem4d  17615  sscres  17792  xpcid  18157  evlfcllem  18189  hofcl  18227  isacs5lem  18511  frmdup3lem  18800  cayleylem2  19350  f1omvdco2  19385  symggen  19407  psgnunilem1  19430  pgp0  19533  sylow3lem2  19565  lsmdisjr  19621  lsmdisj2r  19622  subgdisj2  19629  efgval  19654  frgpuplem  19709  frgpup2  19713  gsumval3  19844  gsumzres  19846  gsum2d2lem  19910  dprdf1  19972  dmdprdsplit2lem  19984  dmdprdsplit2  19985  ablfaclem3  20026  prdsmgp  20067  unitgrp  20299  subdrgint  20719  crng2idl  21198  gsumfsum  21358  pzriprnglem6  21403  chrid  21442  znleval  21471  frgpcyg  21490  ocv1  21595  frlmip  21694  ellspd  21718  psrass1lem  21848  ply1chr  22200  evl1var  22230  pf1mpf  22246  pf1ind  22249  mamuvs2  22300  madurid  22538  baspartn  22848  mretopd  22986  ordtcld1  23091  ordtcld2  23092  leordtvallem1  23104  leordtvallem2  23105  paste  23188  imacmp  23291  cmpsub  23294  unconn  23323  1stckgen  23448  ptbasfi  23475  txcld  23497  ptclsg  23509  txdis1cn  23529  ptrescn  23533  hausdiag  23539  txkgen  23546  xkoptsub  23548  xkococnlem  23553  cnmpt21  23565  cnmpt22  23568  tgqtop  23606  qtoprest  23611  kqdisj  23626  hmeores  23665  hmphindis  23691  pt1hmeo  23700  ptuncnv  23701  ptunhmeo  23702  xpstopnlem1  23703  xkohmeo  23709  alexsublem  23938  ptcmplem2  23947  tmdcn2  23983  cldsubg  24005  qustgplem  24015  tsmsres  24038  ustbas2  24120  ressuss  24157  metreslem  24257  xpsdsval  24276  prdsxmslem2  24424  txmetcnp  24442  tngngp  24549  nrmtngdist  24552  remetdval  24684  cnheibor  24861  evth2  24866  pcoass  24931  ncvspi  25063  iscmet3  25200  rrxip  25297  minveclem2  25333  cmmbl  25442  nulmbl2  25444  volinun  25454  voliunlem1  25458  volsup  25464  ovolioo  25476  uniiccdif  25486  uniioombllem2  25491  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  ismbf3d  25562  itg2uba  25651  itg2i1fseq  25663  itgsplitioo  25746  limcflf  25789  cnplimc  25795  limcun  25803  dvfval  25805  dvres  25819  dvres3a  25822  dvnp1  25834  dvn1  25835  dvexp3  25889  dvsincos  25892  mvth  25904  c1lip2  25910  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgsubstlem  25962  itgsubst  25963  coeeq2  26154  dgreq0  26178  dgrcolem2  26187  vieta1  26227  ulm2  26301  radcnv0  26332  abelthlem2  26349  tanarg  26535  advlogexp  26571  efopn  26574  logtayl  26576  cxpcn3  26665  ang180lem3  26728  quad2  26756  mcubic  26764  binom4  26767  dquart  26770  quart1lem  26772  quart1  26773  quartlem1  26774  asinlem3a  26787  efiatan  26829  tanatan  26836  atanbndlem  26842  dvatan  26852  wilthlem2  26986  ftalem3  26992  ftalem5  26994  basellem3  27000  mumullem2  27097  musum  27108  mpodvdsmulf1o  27111  chtublem  27129  perfectlem2  27148  bposlem6  27207  bposlem9  27210  1lgs  27258  lgs1  27259  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgsquadlem2  27299  lgsquad2lem2  27303  2sqblem  27349  rpvmasum2  27430  log2sumbnd  27462  noetasuplem4  27655  sltlpss  27826  slelss  27827  opphllem3  28683  vtxdun  29416  clwwlknon2num  30041  eucrct2eupth  30181  ex-fpar  30398  nvpi  30603  nvop  30612  phop  30754  minvecolem2  30811  hi01  31032  pjchi  31368  chjidm  31456  mayete3i  31664  ho0val  31686  lnop0  31902  adjbdlnb  32020  pjin2i  32129  mdslmd3i  32268  mdexchi  32271  imadifxp  32537  fcoinver  32540  suppovss  32611  fressupp  32618  supppreima  32621  mptprop  32628  padct  32650  f1od2  32651  fcobijfs  32653  ffsrn  32659  iocinif  32711  difioo  32712  indf1ofs  32796  s2rnOLD  32872  s3rnOLD  32874  cshw1s2  32889  gsummpt2co  32995  gsumhashmul  33008  symgfcoeu  33046  symgcom  33047  pmtrprfv2  33052  pmtrcnel2  33054  tocyc01  33082  cycpmconjv  33106  cycpmconjs  33120  elrgspnlem2  33201  ofldchr  33299  lsmsnorb2  33370  krull  33457  opprqusbas  33466  opprqusplusg  33467  qsdrngi  33473  rgmoddimOLD  33613  ply1degltdimlem  33625  lindsun  33628  dimkerim  33630  fldexttr  33661  constrcon  33771  cos9thpiminplylem3  33781  smatlem  33794  zarcmplem  33878  esumpad2  34053  hasheuni  34082  esumcvg2  34084  esum2dlem  34089  sigapildsys  34159  measxun2  34207  measunl  34213  measinblem  34217  carsgclctunlem1  34315  carsgclctunlem3  34318  sibfof  34338  sitgclg  34340  eulerpartlemgf  34377  probdif  34418  cndprobval  34431  ballotlemic  34505  signsvtn0  34568  signstres  34573  chtvalz  34627  hgt750lemd  34646  bnj1415  35035  f1resrcmplf1d  35084  f1resfz0f1d  35108  revwlk  35119  subfacp1lem1  35173  subfacp1lem3  35176  subfacp1lem5  35178  cvmscld  35267  cvmlift2lem9a  35297  cvmlift2lem9  35305  fwddifnp1  36160  finxpreclem5  37390  ptrest  37620  poimirlem2  37623  poimirlem3  37624  poimirlem6  37627  poimirlem7  37628  poimirlem9  37630  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem24  37645  poimirlem25  37646  poimirlem27  37648  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  voliunnfl  37665  volsupnfl  37666  mbfresfi  37667  itg2addnclem2  37673  itg2addnclem3  37674  ftc1anclem5  37698  dvacos  37706  areacirclem5  37713  cocnv  37726  istotbnd3  37772  ssbnd  37789  disjresdisj  38236  eccnvepres3  38281  symrelim  38557  osumcllem9N  39965  4atexlemex2  40072  cdleme20j  40319  cdlemg47  40737  diaintclN  41059  dibintclN  41168  dihintcl  41345  lclkrlem2e  41512  lclkrlem2p  41523  lcfrlem31  41574  lcmineqlem  42047  sticksstones8  42148  dvun  42354  readdlid  42398  evlsvvval  42558  selvvvval  42580  fsuppssind  42588  prjspnval2  42613  flt4lem  42640  diophin  42767  monotuz  42937  monotoddzzfi  42938  oddcomabszz  42940  fnwe2val  43045  lnmlmic  43084  fiuneneq  43188  cytpval  43198  oaun3  43378  ntrkbimka  44034  ntrneifv2  44076  mnringmulrd  44219  mnringmulrcld  44224  radcnvrat  44310  nzprmdif  44315  binomcxplemnotnn0  44352  ioccncflimc  45890  icocncflimc  45894  stoweidlem50  46055  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem107  46218  lambert0  46895  lamberte  46896  elsprel  47480  reuopreuprim  47531  perfectALTVlem2  47727  dfnbgr6  47861  dfsclnbgr6  47862  restclssep  48908  seposep  48918  iscnrm3rlem8  48939  swapfid  49272  cofuswapf1  49287  cofuswapf2  49288  idfudiag1lem  49516  termcfuncval  49525  ranval  49613  lmddu  49660  initocmd  49662  logb2aval  49757  aacllem  49794