Theorem eqtr3id 2809

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 2769	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2807	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 2155  ax-ext 2732

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

This theorem is used by:  3eqtr3g  2818  csbeq1a  3861  ssdifeq0  4442  pofun  5581  opabbi2dv  5829  cnvsng  6219  csbpredg  6305  funcnvpr  6596  funcnvtp  6597  funcnvqp  6598  fresin  6745  fresaunres2  6748  f1imacnv  6835  foimacnv  6836  funfv  6966  dffv2  6974  fimacnvinrn  7065  rescnvimafod  7067  fsn2  7131  funiunfvf  7247  f1resrcmplf1d  7273  fcof1oinvd  7295  riotaxfrd  7405  f1opw2  7670  fnexALT  7949  fparlem3  8112  fparlem4  8113  fsplitfpar  8116  fvproj  8133  mpocurryd  8268  seqomlem1  8440  seqomlem4  8443  oasuc  8512  oesuclem  8513  omsuc  8514  onasuc  8516  onmsuc  8517  eqerlem  8733  pmresg  8878  fopwdom  9084  sbthlem8  9093  sbthlem9  9094  fodomr  9127  domss2  9135  mapen  9140  cnvfi  9171  fiint  9297  fodomfir  9298  f1opwfi  9324  mapfien  9379  marypha1lem  9404  unxpwdom  9562  cantnfval2  9649  ttrcltr  9696  infxpenlem  10017  djuinf  10192  isf34lem3  10378  isf34lem5  10381  axdc4lem  10458  ttukeylem6  10517  rankcf  10787  tskuni  10793  gruima  10812  dmrecnq  10978  ltexnq  10985  reclem3pr  11059  pn0sr  11111  mulgt0sr  11115  recdiv  11946  2resupmax  13241  max0sub  13249  rexmul  13324  xmulmnf1  13329  xmulm1  13334  prunioo  13535  fseq1p1m1  13654  fzshftral  13671  f1resfz0f1d  13849  seqp1d  14083  seqf1olem2  14107  seqfeq4  14116  binom3  14289  expmulnbnd  14300  discr  14305  bcn2  14384  hashun2  14448  hashun3  14449  hashdif  14479  hashgt12el  14488  hashgt12el2  14489  hashfacen  14520  s2prop  14979  s4prop  14982  s3sndisj  15041  s3iunsndisj  15042  cnrecnv  15253  rddif  15429  amgm2  15458  rlimres  15646  lo1res  15647  iseraltlem2  15771  iseralt  15773  fsumss  15812  fsumcl2lem  15818  isumclim3  15846  fsumcnv  15860  telfsumo  15890  fsumiun  15909  arisum2  15951  geoisum1c  15970  fprodss  16036  fprodser  16037  fprodcl2lem  16038  fprodsplit  16054  fprodn0  16067  fprodcnv  16071  iprodclim3  16088  risefac1  16120  fallfac1  16121  bpolyval  16136  bpoly3  16145  bpoly4  16146  fsumcube  16147  sinhval  16243  cos01bnd  16275  ruclem6  16324  sadadd2lem2  16541  eucalgval  16673  pcid  16966  prmreclem4  17012  4sqlem15  17052  4sqlem16  17053  ramcl  17122  strfv2d  17294  setsid  17300  imasvscafn  17624  xpsff1o  17654  xpsaddlem  17660  xpsvsca  17664  xpsle  17666  mreexexlem2d  17734  mreexexlem4d  17736  sscres  17913  xpcid  18278  evlfcllem  18310  hofcl  18348  isacs5lem  18634  frmdup3lem  18976  cayleylem2  19541  f1omvdco2  19576  symggen  19598  psgnunilem1  19621  pgp0  19724  sylow3lem2  19756  lsmdisjr  19812  lsmdisj2r  19813  subgdisj2  19820  efgval  19845  frgpuplem  19900  frgpup2  19904  gsumval3  20035  gsumzres  20037  gsum2d2lem  20101  dprdf1  20163  dmdprdsplit2lem  20175  dmdprdsplit2  20176  ablfaclem3  20217  prdsmgp  20285  unitgrp  20525  subdrgint  20970  crng2idl  21484  gsumfsum  21648  pzriprnglem6  21700  chrid  21739  znleval  21768  frgpcyg  21787  ofldchr  21790  ocv1  21893  frlmip  21992  ellspd  22016  psrass1lem  22149  evlsvvval  22310  selvvvval  22359  ply1chr  22532  evl1var  22562  pf1mpf  22578  pf1ind  22581  mamuvs2  22629  madurid  22867  baspartn  23180  mretopd  23318  ordtcld1  23423  ordtcld2  23424  leordtvallem1  23436  leordtvallem2  23437  paste  23520  imacmp  23623  cmpsub  23626  unconn  23655  1stckgen  23781  ptbasfi  23808  txcld  23830  ptclsg  23842  txdis1cn  23862  ptrescn  23866  hausdiag  23872  txkgen  23879  xkoptsub  23881  xkococnlem  23886  cnmpt21  23898  cnmpt22  23901  tgqtop  23939  qtoprest  23944  kqdisj  23959  hmeores  23998  hmphindis  24024  pt1hmeo  24033  ptuncnv  24034  ptunhmeo  24035  xpstopnlem1  24036  xkohmeo  24042  alexsublem  24271  ptcmplem2  24280  tmdcn2  24316  cldsubg  24338  qustgplem  24348  tsmsres  24371  ustbas2  24452  ressuss  24489  metreslem  24589  xpsdsval  24608  prdsxmslem2  24756  txmetcnp  24774  tngngp  24881  nrmtngdist  24884  remetdval  25016  cnheibor  25184  evth2  25189  pcoass  25253  ncvspi  25385  iscmet3  25522  rrxip  25619  minveclem2  25655  cmmbl  25763  nulmbl2  25765  volinun  25775  voliunlem1  25779  volsup  25785  ovolioo  25797  uniiccdif  25807  uniioombllem2  25812  uniioombllem3  25814  uniioombllem4  25815  uniioombllem5  25816  ismbf3d  25883  itg2uba  25972  itg2i1fseq  25984  itgsplitioo  26066  limcflf  26109  cnplimc  26115  limcun  26123  dvfval  26125  dvres  26139  dvres3a  26142  dvnp1  26153  dvn1  26154  dvexp3  26206  dvsincos  26209  mvth  26220  c1lip2  26226  dvfsumlem2  26255  itgsubstlem  26276  itgsubst  26277  coeeq2  26469  dgreq0  26492  dgrcolem2  26501  vieta1  26545  ulm2  26622  radcnv0  26653  abelthlem2  26669  tanarg  26857  advlogexp  26893  efopn  26896  logtayl  26898  cxpcn3  26986  ang180lem3  27049  quad2  27077  mcubic  27085  binom4  27088  dquart  27091  quart1lem  27093  quart1  27094  quartlem1  27095  asinlem3a  27108  efiatan  27150  tanatan  27157  atanbndlem  27163  dvatan  27173  wilthlem2  27306  ftalem3  27312  ftalem5  27314  basellem3  27320  mumullem2  27417  musum  27428  mpodvdsmulf1o  27431  ppiub  27441  chtublem  27448  perfectlem2  27467  bposlem6  27526  bposlem9  27529  1lgs  27577  lgs1  27578  lgseisenlem1  27612  lgseisenlem2  27613  lgseisenlem3  27614  lgsquadlem2  27618  lgsquad2lem2  27622  2sqblem  27668  rpvmasum2  27749  log2sumbnd  27781  noetasuplem4  27973  ltslpss  28174  leslss  28175  bdayfinbndlem1  28733  z12shalf  28746  opphllem3  29105  prlngpln3  29307  vtxdun  29942  revwlk  30147  clwwlknon2num  30576  eucrct2eupth  30726  ex-fpar  30943  nvpi  31149  nvop  31158  phop  31300  minvecolem2  31357  hi01  31578  pjchi  31914  chjidm  32002  mayete3i  32210  ho0val  32232  lnop0  32448  adjbdlnb  32566  pjin2i  32675  mdslmd3i  32814  mdexchi  32817  imadifxp  33075  fcoinver  33078  suppovss  33154  fressupp  33161  supppreima  33164  mptprop  33171  f1od2  33191  fcobijfs  33193  ffsrn  33200  iocinif  33253  difioo  33254  indf1ofs  33313  cshw1s2  33401  gsummpt2co  33489  gsumhashmul  33508  gsummulsubdishift1s  33511  gsummulsubdishift2s  33512  symgfcoeu  33523  symgcom  33524  pmtrprfv2  33529  pmtrcnel2  33531  tocyc01  33559  cycpmconjv  33583  cycpmconjs  33597  elrgspnlem2  33684  lsmsnorb2  33826  krull  33882  opprqusbas  33891  opprqusplusg  33892  qsdrngi  33898  psrgsum  34059  psrmonprod  34063  ply1degltdimlem  34133  lindsun  34136  dimkerim  34138  fldexttr  34169  constrcon  34285  cos9thpiminplylem3  34295  smatlem  34308  zarcmplem  34392  esumpad2  34567  hasheuni  34596  esumcvg2  34598  esum2dlem  34603  sigapildsys  34674  measxun2  34722  measunl  34728  measinblem  34732  carsgclctunlem1  34829  carsgclctunlem3  34832  sibfof  34852  sitgclg  34854  eulerpartlemgf  34891  probdif  34932  cndprobval  34945  ballotlemic  35019  signsvtn0  35079  signstres  35084  chtvalz  35138  hgt750lemd  35157  bnj1415  35548  subfacp1lem1  35759  subfacp1lem3  35762  subfacp1lem5  35764  cvmscld  35853  cvmlift2lem9a  35883  cvmlift2lem9  35891  fwddifnp1  36746  dfttc4  37150  finxpreclem5  38150  ptrest  38369  poimirlem2  38372  poimirlem3  38373  poimirlem6  38376  poimirlem7  38377  poimirlem9  38379  poimirlem11  38381  poimirlem12  38382  poimirlem16  38386  poimirlem17  38387  poimirlem19  38389  poimirlem20  38390  poimirlem24  38394  poimirlem25  38395  poimirlem27  38397  poimirlem28  38398  poimirlem29  38399  poimirlem31  38401  voliunnfl  38414  volsupnfl  38415  mbfresfi  38416  itg2addnclem2  38422  itg2addnclem3  38423  ftc1anclem5  38447  dvacos  38455  areacirclem5  38462  cocnv  38476  istotbnd3  38522  ssbnd  38539  disjresdisj  38993  eccnvepres3  39041  dfblockliftmap2  39210  symrelim  39392  osumcllem9N  40838  4atexlemex2  40945  cdleme20j  41192  cdlemg47  41610  diaintclN  41932  dibintclN  42041  dihintcl  42218  lclkrlem2e  42385  lclkrlem2p  42396  lcfrlem31  42447  lcmineqlem  42919  sticksstones8  43020  dvun  43235  readdlid  43279  fsuppssind  43440  prjspnval2  43465  flt4lem  43492  diophin  43618  monotuz  43783  monotoddzzfi  43784  oddcomabszz  43786  fnwe2val  43891  lnmlmic  43930  fiuneneq  44034  cytpval  44044  oaun3  44224  ntrkbimka  44879  ntrneifv2  44921  mnringmulrd  45062  mnringmulrcld  45067  radcnvrat  45139  nzprmdif  45144  binomcxplemnotnn0  45181  limsupvaluz  46537  ioccncflimc  46714  icocncflimc  46718  stoweidlem50  46879  fourierdlem48  46983  fourierdlem49  46984  fourierdlem89  47024  fourierdlem90  47025  fourierdlem91  47026  fourierdlem107  47042  lambert0  47756  lamberte  47757  elsprel  48376  reuopreuprim  48427  perfectALTVlem2  48639  dfnbgr6  48774  dfsclnbgr6  48775  smprngprmrng  49255  restclssep  49843  seposep  49853  iscnrm3rlem8  49874  swapfid  50206  cofuswapf1  50221  cofuswapf2  50222  idfudiag1lem  50450  termcfuncval  50459  ranval  50547  lmddu  50594  initocmd  50596  logb2aval  50694  aacllem  50773