Theorem eqtr3id 2778

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

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

This theorem is referenced by:  3eqtr3g  2787  csbeq1a  3867  ssdifeq0  4440  pofun  5549  opabbi2dv  5796  cnvsng  6176  csbpredg  6259  funcnvpr  6548  funcnvtp  6549  funcnvqp  6550  f1imadifssran  6572  fresin  6697  fresaunres2  6700  f1imacnv  6784  foimacnv  6785  funfv  6914  dffv2  6922  fimacnvinrn  7009  rescnvimafod  7011  fsn2  7074  funiunfvf  7189  fcof1oinvd  7234  riotaxfrd  7344  f1opw2  7608  fnexALT  7893  fparlem3  8054  fparlem4  8055  fsplitfpar  8058  fvproj  8074  mpocurryd  8209  seqomlem1  8379  seqomlem4  8382  oasuc  8449  oesuclem  8450  omsuc  8451  onasuc  8453  onmsuc  8454  eqerlem  8667  pmresg  8804  fopwdom  9009  sbthlem8  9018  sbthlem9  9019  fodomr  9052  domss2  9060  mapen  9065  cnvfi  9100  enp1iOLD  9183  xpfiOLD  9228  fiint  9235  fiintOLD  9236  fodomfir  9237  f1opwfi  9265  mapfien  9317  marypha1lem  9342  unxpwdom  9500  cantnfval2  9584  ttrcltr  9631  infxpenlem  9926  djuinf  10102  isf34lem3  10288  isf34lem5  10291  axdc4lem  10368  ttukeylem6  10427  rankcf  10690  tskuni  10696  gruima  10715  dmrecnq  10881  ltexnq  10888  reclem3pr  10962  pn0sr  11014  mulgt0sr  11018  recdiv  11848  2resupmax  13108  max0sub  13116  rexmul  13191  xmulmnf1  13196  xmulm1  13201  prunioo  13402  fseq1p1m1  13519  fzshftral  13536  seqp1d  13943  seqf1olem2  13967  seqfeq4  13976  binom3  14149  expmulnbnd  14160  discr  14165  bcn2  14244  hashun2  14308  hashun3  14309  hashdif  14338  hashgt12el  14347  hashgt12el2  14348  hashfacen  14379  s2prop  14832  s4prop  14835  s3sndisj  14892  s3iunsndisj  14893  cnrecnv  15090  rddif  15266  amgm2  15295  rlimres  15483  lo1res  15484  iseraltlem2  15608  iseralt  15610  fsumss  15650  fsumcl2lem  15656  isumclim3  15684  fsumcnv  15698  telfsumo  15727  fsumiun  15746  arisum2  15786  geoisum1c  15805  fprodss  15873  fprodser  15874  fprodcl2lem  15875  fprodsplit  15891  fprodn0  15904  fprodcnv  15908  iprodclim3  15925  risefac1  15958  fallfac1  15959  bpolyval  15974  bpoly3  15983  bpoly4  15984  fsumcube  15985  sinhval  16081  cos01bnd  16113  ruclem6  16162  sadadd2lem2  16379  eucalgval  16511  pcid  16803  prmreclem4  16849  4sqlem15  16889  4sqlem16  16890  ramcl  16959  strfv2d  17130  setsid  17136  imasvscafn  17459  xpsff1o  17489  xpsaddlem  17495  xpsvsca  17499  xpsle  17501  mreexexlem2d  17569  mreexexlem4d  17571  sscres  17748  xpcid  18113  evlfcllem  18145  hofcl  18183  isacs5lem  18469  frmdup3lem  18758  cayleylem2  19310  f1omvdco2  19345  symggen  19367  psgnunilem1  19390  pgp0  19493  sylow3lem2  19525  lsmdisjr  19581  lsmdisj2r  19582  subgdisj2  19589  efgval  19614  frgpuplem  19669  frgpup2  19673  gsumval3  19804  gsumzres  19806  gsum2d2lem  19870  dprdf1  19932  dmdprdsplit2lem  19944  dmdprdsplit2  19945  ablfaclem3  19986  prdsmgp  20054  unitgrp  20286  subdrgint  20706  crng2idl  21206  gsumfsum  21359  pzriprnglem6  21411  chrid  21450  znleval  21479  frgpcyg  21498  ofldchr  21501  ocv1  21604  frlmip  21703  ellspd  21727  psrass1lem  21857  ply1chr  22209  evl1var  22239  pf1mpf  22255  pf1ind  22258  mamuvs2  22309  madurid  22547  baspartn  22857  mretopd  22995  ordtcld1  23100  ordtcld2  23101  leordtvallem1  23113  leordtvallem2  23114  paste  23197  imacmp  23300  cmpsub  23303  unconn  23332  1stckgen  23457  ptbasfi  23484  txcld  23506  ptclsg  23518  txdis1cn  23538  ptrescn  23542  hausdiag  23548  txkgen  23555  xkoptsub  23557  xkococnlem  23562  cnmpt21  23574  cnmpt22  23577  tgqtop  23615  qtoprest  23620  kqdisj  23635  hmeores  23674  hmphindis  23700  pt1hmeo  23709  ptuncnv  23710  ptunhmeo  23711  xpstopnlem1  23712  xkohmeo  23718  alexsublem  23947  ptcmplem2  23956  tmdcn2  23992  cldsubg  24014  qustgplem  24024  tsmsres  24047  ustbas2  24129  ressuss  24166  metreslem  24266  xpsdsval  24285  prdsxmslem2  24433  txmetcnp  24451  tngngp  24558  nrmtngdist  24561  remetdval  24693  cnheibor  24870  evth2  24875  pcoass  24940  ncvspi  25072  iscmet3  25209  rrxip  25306  minveclem2  25342  cmmbl  25451  nulmbl2  25453  volinun  25463  voliunlem1  25467  volsup  25473  ovolioo  25485  uniiccdif  25495  uniioombllem2  25500  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  ismbf3d  25571  itg2uba  25660  itg2i1fseq  25672  itgsplitioo  25755  limcflf  25798  cnplimc  25804  limcun  25812  dvfval  25814  dvres  25828  dvres3a  25831  dvnp1  25843  dvn1  25844  dvexp3  25898  dvsincos  25901  mvth  25913  c1lip2  25919  dvfsumlem2  25949  dvfsumlem2OLD  25950  itgsubstlem  25971  itgsubst  25972  coeeq2  26163  dgreq0  26187  dgrcolem2  26196  vieta1  26236  ulm2  26310  radcnv0  26341  abelthlem2  26358  tanarg  26544  advlogexp  26580  efopn  26583  logtayl  26585  cxpcn3  26674  ang180lem3  26737  quad2  26765  mcubic  26773  binom4  26776  dquart  26779  quart1lem  26781  quart1  26782  quartlem1  26783  asinlem3a  26796  efiatan  26838  tanatan  26845  atanbndlem  26851  dvatan  26861  wilthlem2  26995  ftalem3  27001  ftalem5  27003  basellem3  27009  mumullem2  27106  musum  27117  mpodvdsmulf1o  27120  chtublem  27138  perfectlem2  27157  bposlem6  27216  bposlem9  27219  1lgs  27267  lgs1  27268  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgsquadlem2  27308  lgsquad2lem2  27312  2sqblem  27358  rpvmasum2  27439  log2sumbnd  27471  noetasuplem4  27664  sltlpss  27840  slelss  27841  zs12half  28375  opphllem3  28712  vtxdun  29445  clwwlknon2num  30067  eucrct2eupth  30207  ex-fpar  30424  nvpi  30629  nvop  30638  phop  30780  minvecolem2  30837  hi01  31058  pjchi  31394  chjidm  31482  mayete3i  31690  ho0val  31712  lnop0  31928  adjbdlnb  32046  pjin2i  32155  mdslmd3i  32294  mdexchi  32297  imadifxp  32563  fcoinver  32566  suppovss  32637  fressupp  32644  supppreima  32647  mptprop  32654  padct  32676  f1od2  32677  fcobijfs  32679  ffsrn  32685  iocinif  32737  difioo  32738  indf1ofs  32822  s2rnOLD  32898  s3rnOLD  32900  cshw1s2  32915  gsummpt2co  33014  gsumhashmul  33027  symgfcoeu  33037  symgcom  33038  pmtrprfv2  33043  pmtrcnel2  33045  tocyc01  33073  cycpmconjv  33097  cycpmconjs  33111  elrgspnlem2  33196  lsmsnorb2  33342  krull  33429  opprqusbas  33438  opprqusplusg  33439  qsdrngi  33445  rgmoddimOLD  33585  ply1degltdimlem  33597  lindsun  33600  dimkerim  33602  fldexttr  33633  constrcon  33743  cos9thpiminplylem3  33753  smatlem  33766  zarcmplem  33850  esumpad2  34025  hasheuni  34054  esumcvg2  34056  esum2dlem  34061  sigapildsys  34131  measxun2  34179  measunl  34185  measinblem  34189  carsgclctunlem1  34287  carsgclctunlem3  34290  sibfof  34310  sitgclg  34312  eulerpartlemgf  34349  probdif  34390  cndprobval  34403  ballotlemic  34477  signsvtn0  34540  signstres  34545  chtvalz  34599  hgt750lemd  34618  bnj1415  35007  f1resrcmplf1d  35056  f1resfz0f1d  35089  revwlk  35100  subfacp1lem1  35154  subfacp1lem3  35157  subfacp1lem5  35159  cvmscld  35248  cvmlift2lem9a  35278  cvmlift2lem9  35286  fwddifnp1  36141  finxpreclem5  37371  ptrest  37601  poimirlem2  37604  poimirlem3  37605  poimirlem6  37608  poimirlem7  37609  poimirlem9  37611  poimirlem11  37613  poimirlem12  37614  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem24  37626  poimirlem25  37627  poimirlem27  37629  poimirlem28  37630  poimirlem29  37631  poimirlem31  37633  voliunnfl  37646  volsupnfl  37647  mbfresfi  37648  itg2addnclem2  37654  itg2addnclem3  37655  ftc1anclem5  37679  dvacos  37687  areacirclem5  37694  cocnv  37707  istotbnd3  37753  ssbnd  37770  disjresdisj  38217  eccnvepres3  38262  symrelim  38538  osumcllem9N  39946  4atexlemex2  40053  cdleme20j  40300  cdlemg47  40718  diaintclN  41040  dibintclN  41149  dihintcl  41326  lclkrlem2e  41493  lclkrlem2p  41504  lcfrlem31  41555  lcmineqlem  42028  sticksstones8  42129  dvun  42335  readdlid  42379  evlsvvval  42539  selvvvval  42561  fsuppssind  42569  prjspnval2  42594  flt4lem  42621  diophin  42748  monotuz  42917  monotoddzzfi  42918  oddcomabszz  42920  fnwe2val  43025  lnmlmic  43064  fiuneneq  43168  cytpval  43178  oaun3  43358  ntrkbimka  44014  ntrneifv2  44056  mnringmulrd  44199  mnringmulrcld  44204  radcnvrat  44290  nzprmdif  44295  binomcxplemnotnn0  44332  ioccncflimc  45870  icocncflimc  45874  stoweidlem50  46035  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem107  46198  lambert0  46875  lamberte  46876  elsprel  47463  reuopreuprim  47514  perfectALTVlem2  47710  dfnbgr6  47845  dfsclnbgr6  47846  restclssep  48904  seposep  48914  iscnrm3rlem8  48935  swapfid  49268  cofuswapf1  49283  cofuswapf2  49284  idfudiag1lem  49512  termcfuncval  49521  ranval  49609  lmddu  49656  initocmd  49658  logb2aval  49753  aacllem  49790