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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  3eqtr3g  2794  csbeq1a  3851  ssdifeq0  4426  pofun  5557  opabbi2dv  5804  cnvsng  6187  csbpredg  6271  funcnvpr  6560  funcnvtp  6561  funcnvqp  6562  f1imadifssran  6584  fresin  6709  fresaunres2  6712  f1imacnv  6796  foimacnv  6797  funfv  6927  dffv2  6935  fimacnvinrn  7023  rescnvimafod  7025  fsn2  7089  funiunfvf  7204  fcof1oinvd  7248  riotaxfrd  7358  f1opw2  7622  fnexALT  7904  fparlem3  8064  fparlem4  8065  fsplitfpar  8068  fvproj  8084  mpocurryd  8219  seqomlem1  8389  seqomlem4  8392  oasuc  8459  oesuclem  8460  omsuc  8461  onasuc  8463  onmsuc  8464  eqerlem  8679  pmresg  8818  fopwdom  9023  sbthlem8  9032  sbthlem9  9033  fodomr  9066  domss2  9074  mapen  9079  cnvfi  9110  fiint  9237  fodomfir  9238  f1opwfi  9266  mapfien  9321  marypha1lem  9346  unxpwdom  9504  cantnfval2  9590  ttrcltr  9637  infxpenlem  9935  djuinf  10111  isf34lem3  10297  isf34lem5  10300  axdc4lem  10377  ttukeylem6  10436  rankcf  10700  tskuni  10706  gruima  10725  dmrecnq  10891  ltexnq  10898  reclem3pr  10972  pn0sr  11024  mulgt0sr  11028  recdiv  11861  2resupmax  13140  max0sub  13148  rexmul  13223  xmulmnf1  13228  xmulm1  13233  prunioo  13434  fseq1p1m1  13552  fzshftral  13569  seqp1d  13980  seqf1olem2  14004  seqfeq4  14013  binom3  14186  expmulnbnd  14197  discr  14202  bcn2  14281  hashun2  14345  hashun3  14346  hashdif  14375  hashgt12el  14384  hashgt12el2  14385  hashfacen  14416  s2prop  14869  s4prop  14872  s3sndisj  14929  s3iunsndisj  14930  cnrecnv  15127  rddif  15303  amgm2  15332  rlimres  15520  lo1res  15521  iseraltlem2  15645  iseralt  15647  fsumss  15687  fsumcl2lem  15693  isumclim3  15721  fsumcnv  15735  telfsumo  15765  fsumiun  15784  arisum2  15826  geoisum1c  15845  fprodss  15913  fprodser  15914  fprodcl2lem  15915  fprodsplit  15931  fprodn0  15944  fprodcnv  15948  iprodclim3  15965  risefac1  15998  fallfac1  15999  bpolyval  16014  bpoly3  16023  bpoly4  16024  fsumcube  16025  sinhval  16121  cos01bnd  16153  ruclem6  16202  sadadd2lem2  16419  eucalgval  16551  pcid  16844  prmreclem4  16890  4sqlem15  16930  4sqlem16  16931  ramcl  17000  strfv2d  17171  setsid  17177  imasvscafn  17501  xpsff1o  17531  xpsaddlem  17537  xpsvsca  17541  xpsle  17543  mreexexlem2d  17611  mreexexlem4d  17613  sscres  17790  xpcid  18155  evlfcllem  18187  hofcl  18225  isacs5lem  18511  frmdup3lem  18834  cayleylem2  19388  f1omvdco2  19423  symggen  19445  psgnunilem1  19468  pgp0  19571  sylow3lem2  19603  lsmdisjr  19659  lsmdisj2r  19660  subgdisj2  19667  efgval  19692  frgpuplem  19747  frgpup2  19751  gsumval3  19882  gsumzres  19884  gsum2d2lem  19948  dprdf1  20010  dmdprdsplit2lem  20022  dmdprdsplit2  20023  ablfaclem3  20064  prdsmgp  20132  unitgrp  20363  subdrgint  20780  crng2idl  21279  gsumfsum  21414  pzriprnglem6  21466  chrid  21505  znleval  21534  frgpcyg  21553  ofldchr  21556  ocv1  21659  frlmip  21758  ellspd  21782  psrass1lem  21912  evlsvvval  22071  ply1chr  22271  evl1var  22301  pf1mpf  22317  pf1ind  22320  mamuvs2  22371  madurid  22609  baspartn  22919  mretopd  23057  ordtcld1  23162  ordtcld2  23163  leordtvallem1  23175  leordtvallem2  23176  paste  23259  imacmp  23362  cmpsub  23365  unconn  23394  1stckgen  23519  ptbasfi  23546  txcld  23568  ptclsg  23580  txdis1cn  23600  ptrescn  23604  hausdiag  23610  txkgen  23617  xkoptsub  23619  xkococnlem  23624  cnmpt21  23636  cnmpt22  23639  tgqtop  23677  qtoprest  23682  kqdisj  23697  hmeores  23736  hmphindis  23762  pt1hmeo  23771  ptuncnv  23772  ptunhmeo  23773  xpstopnlem1  23774  xkohmeo  23780  alexsublem  24009  ptcmplem2  24018  tmdcn2  24054  cldsubg  24076  qustgplem  24086  tsmsres  24109  ustbas2  24190  ressuss  24227  metreslem  24327  xpsdsval  24346  prdsxmslem2  24494  txmetcnp  24512  tngngp  24619  nrmtngdist  24622  remetdval  24754  cnheibor  24922  evth2  24927  pcoass  24991  ncvspi  25123  iscmet3  25260  rrxip  25357  minveclem2  25393  cmmbl  25501  nulmbl2  25503  volinun  25513  voliunlem1  25517  volsup  25523  ovolioo  25535  uniiccdif  25545  uniioombllem2  25550  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  ismbf3d  25621  itg2uba  25710  itg2i1fseq  25722  itgsplitioo  25805  limcflf  25848  cnplimc  25854  limcun  25862  dvfval  25864  dvres  25878  dvres3a  25881  dvnp1  25892  dvn1  25893  dvexp3  25945  dvsincos  25948  mvth  25959  c1lip2  25965  dvfsumlem2  25994  itgsubstlem  26015  itgsubst  26016  coeeq2  26207  dgreq0  26230  dgrcolem2  26239  vieta1  26278  ulm2  26350  radcnv0  26381  abelthlem2  26397  tanarg  26583  advlogexp  26619  efopn  26622  logtayl  26624  cxpcn3  26712  ang180lem3  26775  quad2  26803  mcubic  26811  binom4  26814  dquart  26817  quart1lem  26819  quart1  26820  quartlem1  26821  asinlem3a  26834  efiatan  26876  tanatan  26883  atanbndlem  26889  dvatan  26899  wilthlem2  27032  ftalem3  27038  ftalem5  27040  basellem3  27046  mumullem2  27143  musum  27154  mpodvdsmulf1o  27157  chtublem  27174  perfectlem2  27193  bposlem6  27252  bposlem9  27255  1lgs  27303  lgs1  27304  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgsquadlem2  27344  lgsquad2lem2  27348  2sqblem  27394  rpvmasum2  27475  log2sumbnd  27507  noetasuplem4  27700  ltslpss  27900  leslss  27901  bdayfinbndlem1  28459  z12shalf  28472  opphllem3  28817  vtxdun  29550  clwwlknon2num  30175  eucrct2eupth  30315  ex-fpar  30532  nvpi  30738  nvop  30747  phop  30889  minvecolem2  30946  hi01  31167  pjchi  31503  chjidm  31591  mayete3i  31799  ho0val  31821  lnop0  32037  adjbdlnb  32155  pjin2i  32264  mdslmd3i  32403  mdexchi  32406  imadifxp  32671  fcoinver  32674  suppovss  32754  fressupp  32761  supppreima  32764  mptprop  32771  f1od2  32792  fcobijfs  32794  ffsrn  32801  iocinif  32854  difioo  32855  indf1ofs  32926  s2rnOLD  33004  s3rnOLD  33006  cshw1s2  33020  gsummpt2co  33109  gsumhashmul  33128  gsummulsubdishift1s  33131  gsummulsubdishift2s  33132  symgfcoeu  33143  symgcom  33144  pmtrprfv2  33149  pmtrcnel2  33151  tocyc01  33179  cycpmconjv  33203  cycpmconjs  33217  elrgspnlem2  33304  lsmsnorb2  33452  krull  33539  opprqusbas  33548  opprqusplusg  33549  qsdrngi  33555  psrgsum  33692  psrmonprod  33696  ply1degltdimlem  33766  lindsun  33769  dimkerim  33771  fldexttr  33802  constrcon  33918  cos9thpiminplylem3  33928  smatlem  33941  zarcmplem  34025  esumpad2  34200  hasheuni  34229  esumcvg2  34231  esum2dlem  34236  sigapildsys  34306  measxun2  34354  measunl  34360  measinblem  34364  carsgclctunlem1  34461  carsgclctunlem3  34464  sibfof  34484  sitgclg  34486  eulerpartlemgf  34523  probdif  34564  cndprobval  34577  ballotlemic  34651  signsvtn0  34714  signstres  34719  chtvalz  34773  hgt750lemd  34792  bnj1415  35180  f1resrcmplf1d  35230  f1resfz0f1d  35296  revwlk  35307  subfacp1lem1  35361  subfacp1lem3  35364  subfacp1lem5  35366  cvmscld  35455  cvmlift2lem9a  35485  cvmlift2lem9  35493  fwddifnp1  36347  dfttc4  36712  finxpreclem5  37711  ptrest  37940  poimirlem2  37943  poimirlem3  37944  poimirlem6  37947  poimirlem7  37948  poimirlem9  37950  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem24  37965  poimirlem25  37966  poimirlem27  37968  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  voliunnfl  37985  volsupnfl  37986  mbfresfi  37987  itg2addnclem2  37993  itg2addnclem3  37994  ftc1anclem5  38018  dvacos  38026  areacirclem5  38033  cocnv  38046  istotbnd3  38092  ssbnd  38109  disjresdisj  38565  eccnvepres3  38613  dfblockliftmap2  38782  symrelim  38964  osumcllem9N  40410  4atexlemex2  40517  cdleme20j  40764  cdlemg47  41182  diaintclN  41504  dibintclN  41613  dihintcl  41790  lclkrlem2e  41957  lclkrlem2p  41968  lcfrlem31  42019  lcmineqlem  42491  sticksstones8  42592  dvun  42791  readdlid  42835  selvvvval  43018  fsuppssind  43026  prjspnval2  43051  flt4lem  43078  diophin  43204  monotuz  43369  monotoddzzfi  43370  oddcomabszz  43372  fnwe2val  43477  lnmlmic  43516  fiuneneq  43620  cytpval  43630  oaun3  43810  ntrkbimka  44465  ntrneifv2  44507  mnringmulrd  44650  mnringmulrcld  44655  radcnvrat  44741  nzprmdif  44746  binomcxplemnotnn0  44783  ioccncflimc  46313  icocncflimc  46317  stoweidlem50  46478  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem107  46641  lambert0  47335  lamberte  47336  elsprel  47935  reuopreuprim  47986  perfectALTVlem2  48198  dfnbgr6  48333  dfsclnbgr6  48334  restclssep  49391  seposep  49401  iscnrm3rlem8  49422  swapfid  49754  cofuswapf1  49769  cofuswapf2  49770  idfudiag1lem  49998  termcfuncval  50007  ranval  50095  lmddu  50142  initocmd  50144  logb2aval  50239  aacllem  50276