Theorem eqtr3id 2785

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

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

This theorem is referenced by:  3eqtr3g  2794  csbeq1a  3863  ssdifeq0  4439  pofun  5550  opabbi2dv  5798  cnvsng  6181  csbpredg  6265  funcnvpr  6554  funcnvtp  6555  funcnvqp  6556  f1imadifssran  6578  fresin  6703  fresaunres2  6706  f1imacnv  6790  foimacnv  6791  funfv  6921  dffv2  6929  fimacnvinrn  7016  rescnvimafod  7018  fsn2  7081  funiunfvf  7195  fcof1oinvd  7239  riotaxfrd  7349  f1opw2  7613  fnexALT  7895  fparlem3  8056  fparlem4  8057  fsplitfpar  8060  fvproj  8076  mpocurryd  8211  seqomlem1  8381  seqomlem4  8384  oasuc  8451  oesuclem  8452  omsuc  8453  onasuc  8455  onmsuc  8456  eqerlem  8670  pmresg  8808  fopwdom  9013  sbthlem8  9022  sbthlem9  9023  fodomr  9056  domss2  9064  mapen  9069  cnvfi  9100  fiint  9227  fodomfir  9228  f1opwfi  9256  mapfien  9311  marypha1lem  9336  unxpwdom  9494  cantnfval2  9578  ttrcltr  9625  infxpenlem  9923  djuinf  10099  isf34lem3  10285  isf34lem5  10288  axdc4lem  10365  ttukeylem6  10424  rankcf  10688  tskuni  10694  gruima  10713  dmrecnq  10879  ltexnq  10886  reclem3pr  10960  pn0sr  11012  mulgt0sr  11016  recdiv  11847  2resupmax  13103  max0sub  13111  rexmul  13186  xmulmnf1  13191  xmulm1  13196  prunioo  13397  fseq1p1m1  13514  fzshftral  13531  seqp1d  13941  seqf1olem2  13965  seqfeq4  13974  binom3  14147  expmulnbnd  14158  discr  14163  bcn2  14242  hashun2  14306  hashun3  14307  hashdif  14336  hashgt12el  14345  hashgt12el2  14346  hashfacen  14377  s2prop  14830  s4prop  14833  s3sndisj  14890  s3iunsndisj  14891  cnrecnv  15088  rddif  15264  amgm2  15293  rlimres  15481  lo1res  15482  iseraltlem2  15606  iseralt  15608  fsumss  15648  fsumcl2lem  15654  isumclim3  15682  fsumcnv  15696  telfsumo  15725  fsumiun  15744  arisum2  15784  geoisum1c  15803  fprodss  15871  fprodser  15872  fprodcl2lem  15873  fprodsplit  15889  fprodn0  15902  fprodcnv  15906  iprodclim3  15923  risefac1  15956  fallfac1  15957  bpolyval  15972  bpoly3  15981  bpoly4  15982  fsumcube  15983  sinhval  16079  cos01bnd  16111  ruclem6  16160  sadadd2lem2  16377  eucalgval  16509  pcid  16801  prmreclem4  16847  4sqlem15  16887  4sqlem16  16888  ramcl  16957  strfv2d  17128  setsid  17134  imasvscafn  17458  xpsff1o  17488  xpsaddlem  17494  xpsvsca  17498  xpsle  17500  mreexexlem2d  17568  mreexexlem4d  17570  sscres  17747  xpcid  18112  evlfcllem  18144  hofcl  18182  isacs5lem  18468  frmdup3lem  18791  cayleylem2  19342  f1omvdco2  19377  symggen  19399  psgnunilem1  19422  pgp0  19525  sylow3lem2  19557  lsmdisjr  19613  lsmdisj2r  19614  subgdisj2  19621  efgval  19646  frgpuplem  19701  frgpup2  19705  gsumval3  19836  gsumzres  19838  gsum2d2lem  19902  dprdf1  19964  dmdprdsplit2lem  19976  dmdprdsplit2  19977  ablfaclem3  20018  prdsmgp  20086  unitgrp  20319  subdrgint  20736  crng2idl  21236  gsumfsum  21389  pzriprnglem6  21441  chrid  21480  znleval  21509  frgpcyg  21528  ofldchr  21531  ocv1  21634  frlmip  21733  ellspd  21757  psrass1lem  21888  evlsvvval  22048  ply1chr  22250  evl1var  22280  pf1mpf  22296  pf1ind  22299  mamuvs2  22350  madurid  22588  baspartn  22898  mretopd  23036  ordtcld1  23141  ordtcld2  23142  leordtvallem1  23154  leordtvallem2  23155  paste  23238  imacmp  23341  cmpsub  23344  unconn  23373  1stckgen  23498  ptbasfi  23525  txcld  23547  ptclsg  23559  txdis1cn  23579  ptrescn  23583  hausdiag  23589  txkgen  23596  xkoptsub  23598  xkococnlem  23603  cnmpt21  23615  cnmpt22  23618  tgqtop  23656  qtoprest  23661  kqdisj  23676  hmeores  23715  hmphindis  23741  pt1hmeo  23750  ptuncnv  23751  ptunhmeo  23752  xpstopnlem1  23753  xkohmeo  23759  alexsublem  23988  ptcmplem2  23997  tmdcn2  24033  cldsubg  24055  qustgplem  24065  tsmsres  24088  ustbas2  24169  ressuss  24206  metreslem  24306  xpsdsval  24325  prdsxmslem2  24473  txmetcnp  24491  tngngp  24598  nrmtngdist  24601  remetdval  24733  cnheibor  24910  evth2  24915  pcoass  24980  ncvspi  25112  iscmet3  25249  rrxip  25346  minveclem2  25382  cmmbl  25491  nulmbl2  25493  volinun  25503  voliunlem1  25507  volsup  25513  ovolioo  25525  uniiccdif  25535  uniioombllem2  25540  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  ismbf3d  25611  itg2uba  25700  itg2i1fseq  25712  itgsplitioo  25795  limcflf  25838  cnplimc  25844  limcun  25852  dvfval  25854  dvres  25868  dvres3a  25871  dvnp1  25883  dvn1  25884  dvexp3  25938  dvsincos  25941  mvth  25953  c1lip2  25959  dvfsumlem2  25989  dvfsumlem2OLD  25990  itgsubstlem  26011  itgsubst  26012  coeeq2  26203  dgreq0  26227  dgrcolem2  26236  vieta1  26276  ulm2  26350  radcnv0  26381  abelthlem2  26398  tanarg  26584  advlogexp  26620  efopn  26623  logtayl  26625  cxpcn3  26714  ang180lem3  26777  quad2  26805  mcubic  26813  binom4  26816  dquart  26819  quart1lem  26821  quart1  26822  quartlem1  26823  asinlem3a  26836  efiatan  26878  tanatan  26885  atanbndlem  26891  dvatan  26901  wilthlem2  27035  ftalem3  27041  ftalem5  27043  basellem3  27049  mumullem2  27146  musum  27157  mpodvdsmulf1o  27160  chtublem  27178  perfectlem2  27197  bposlem6  27256  bposlem9  27259  1lgs  27307  lgs1  27308  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgsquadlem2  27348  lgsquad2lem2  27352  2sqblem  27398  rpvmasum2  27479  log2sumbnd  27511  noetasuplem4  27704  ltslpss  27904  leslss  27905  bdayfinbndlem1  28463  z12shalf  28476  opphllem3  28821  vtxdun  29555  clwwlknon2num  30180  eucrct2eupth  30320  ex-fpar  30537  nvpi  30742  nvop  30751  phop  30893  minvecolem2  30950  hi01  31171  pjchi  31507  chjidm  31595  mayete3i  31803  ho0val  31825  lnop0  32041  adjbdlnb  32159  pjin2i  32268  mdslmd3i  32407  mdexchi  32410  imadifxp  32676  fcoinver  32679  suppovss  32760  fressupp  32767  supppreima  32770  mptprop  32777  padct  32797  f1od2  32798  fcobijfs  32800  ffsrn  32807  iocinif  32861  difioo  32862  indf1ofs  32948  s2rnOLD  33026  s3rnOLD  33028  cshw1s2  33042  gsummpt2co  33131  gsumhashmul  33150  gsummulsubdishift1s  33153  gsummulsubdishift2s  33154  symgfcoeu  33164  symgcom  33165  pmtrprfv2  33170  pmtrcnel2  33172  tocyc01  33200  cycpmconjv  33224  cycpmconjs  33238  elrgspnlem2  33325  lsmsnorb2  33473  krull  33560  opprqusbas  33569  opprqusplusg  33570  qsdrngi  33576  rgmoddimOLD  33767  ply1degltdimlem  33779  lindsun  33782  dimkerim  33784  fldexttr  33815  constrcon  33931  cos9thpiminplylem3  33941  smatlem  33954  zarcmplem  34038  esumpad2  34213  hasheuni  34242  esumcvg2  34244  esum2dlem  34249  sigapildsys  34319  measxun2  34367  measunl  34373  measinblem  34377  carsgclctunlem1  34474  carsgclctunlem3  34477  sibfof  34497  sitgclg  34499  eulerpartlemgf  34536  probdif  34577  cndprobval  34590  ballotlemic  34664  signsvtn0  34727  signstres  34732  chtvalz  34786  hgt750lemd  34805  bnj1415  35194  f1resrcmplf1d  35243  f1resfz0f1d  35308  revwlk  35319  subfacp1lem1  35373  subfacp1lem3  35376  subfacp1lem5  35378  cvmscld  35467  cvmlift2lem9a  35497  cvmlift2lem9  35505  fwddifnp1  36359  finxpreclem5  37600  ptrest  37820  poimirlem2  37823  poimirlem3  37824  poimirlem6  37827  poimirlem7  37828  poimirlem9  37830  poimirlem11  37832  poimirlem12  37833  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem24  37845  poimirlem25  37846  poimirlem27  37848  poimirlem28  37849  poimirlem29  37850  poimirlem31  37852  voliunnfl  37865  volsupnfl  37866  mbfresfi  37867  itg2addnclem2  37873  itg2addnclem3  37874  ftc1anclem5  37898  dvacos  37906  areacirclem5  37913  cocnv  37926  istotbnd3  37972  ssbnd  37989  disjresdisj  38440  eccnvepres3  38485  dfblockliftmap2  38635  symrelim  38816  osumcllem9N  40224  4atexlemex2  40331  cdleme20j  40578  cdlemg47  40996  diaintclN  41318  dibintclN  41427  dihintcl  41604  lclkrlem2e  41771  lclkrlem2p  41782  lcfrlem31  41833  lcmineqlem  42306  sticksstones8  42407  dvun  42614  readdlid  42658  selvvvval  42828  fsuppssind  42836  prjspnval2  42861  flt4lem  42888  diophin  43014  monotuz  43183  monotoddzzfi  43184  oddcomabszz  43186  fnwe2val  43291  lnmlmic  43330  fiuneneq  43434  cytpval  43444  oaun3  43624  ntrkbimka  44279  ntrneifv2  44321  mnringmulrd  44464  mnringmulrcld  44469  radcnvrat  44555  nzprmdif  44560  binomcxplemnotnn0  44597  ioccncflimc  46129  icocncflimc  46133  stoweidlem50  46294  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem107  46457  lambert0  47133  lamberte  47134  elsprel  47721  reuopreuprim  47772  perfectALTVlem2  47968  dfnbgr6  48103  dfsclnbgr6  48104  restclssep  49161  seposep  49171  iscnrm3rlem8  49192  swapfid  49524  cofuswapf1  49539  cofuswapf2  49540  idfudiag1lem  49768  termcfuncval  49777  ranval  49865  lmddu  49912  initocmd  49914  logb2aval  50009  aacllem  50046