Theorem eqtr3id 2815

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 2775	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2813	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 2156  ax-ext 2738

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

This theorem is used by:  3eqtr3g  2824  csbeq1a  3870  ssdifeq0  4452  pofun  5592  opabbi2dv  5840  cnvsng  6229  csbpredg  6315  funcnvpr  6605  funcnvtp  6606  funcnvqp  6607  fresin  6754  fresaunres2  6757  f1imacnv  6844  foimacnv  6845  funfv  6975  dffv2  6983  fimacnvinrn  7073  rescnvimafod  7075  fsn2  7139  funiunfvf  7254  f1resrcmplf1d  7280  fcof1oinvd  7302  riotaxfrd  7414  f1opw2  7678  fnexALT  7957  fparlem3  8118  fparlem4  8119  fsplitfpar  8122  fvproj  8139  mpocurryd  8274  seqomlem1  8446  seqomlem4  8449  oasuc  8518  oesuclem  8519  omsuc  8520  onasuc  8522  onmsuc  8523  eqerlem  8739  pmresg  8877  fopwdom  9083  sbthlem8  9092  sbthlem9  9093  fodomr  9126  domss2  9134  mapen  9139  cnvfi  9170  fiint  9296  fodomfir  9297  f1opwfi  9323  mapfien  9378  marypha1lem  9403  unxpwdom  9561  cantnfval2  9648  ttrcltr  9695  infxpenlem  10016  djuinf  10191  isf34lem3  10377  isf34lem5  10380  axdc4lem  10457  ttukeylem6  10516  rankcf  10780  tskuni  10786  gruima  10805  dmrecnq  10971  ltexnq  10978  reclem3pr  11052  pn0sr  11104  mulgt0sr  11108  recdiv  11939  2resupmax  13232  max0sub  13240  rexmul  13315  xmulmnf1  13320  xmulm1  13325  prunioo  13526  fseq1p1m1  13645  fzshftral  13662  f1resfz0f1d  13840  seqp1d  14074  seqf1olem2  14098  seqfeq4  14107  binom3  14280  expmulnbnd  14291  discr  14296  bcn2  14375  hashun2  14439  hashun3  14440  hashdif  14470  hashgt12el  14479  hashgt12el2  14480  hashfacen  14511  s2prop  14970  s4prop  14973  s3sndisj  15030  s3iunsndisj  15031  cnrecnv  15242  rddif  15418  amgm2  15447  rlimres  15635  lo1res  15636  iseraltlem2  15760  iseralt  15762  fsumss  15802  fsumcl2lem  15808  isumclim3  15836  fsumcnv  15850  telfsumo  15880  fsumiun  15899  arisum2  15941  geoisum1c  15960  fprodss  16028  fprodser  16029  fprodcl2lem  16030  fprodsplit  16046  fprodn0  16059  fprodcnv  16063  iprodclim3  16080  risefac1  16112  fallfac1  16113  bpolyval  16128  bpoly3  16137  bpoly4  16138  fsumcube  16139  sinhval  16235  cos01bnd  16267  ruclem6  16316  sadadd2lem2  16533  eucalgval  16665  pcid  16958  prmreclem4  17004  4sqlem15  17044  4sqlem16  17045  ramcl  17114  strfv2d  17286  setsid  17292  imasvscafn  17616  xpsff1o  17646  xpsaddlem  17652  xpsvsca  17656  xpsle  17658  mreexexlem2d  17726  mreexexlem4d  17728  sscres  17905  xpcid  18270  evlfcllem  18302  hofcl  18340  isacs5lem  18626  frmdup3lem  18950  cayleylem2  19508  f1omvdco2  19543  symggen  19565  psgnunilem1  19588  pgp0  19691  sylow3lem2  19723  lsmdisjr  19779  lsmdisj2r  19780  subgdisj2  19787  efgval  19812  frgpuplem  19867  frgpup2  19871  gsumval3  20002  gsumzres  20004  gsum2d2lem  20068  dprdf1  20130  dmdprdsplit2lem  20142  dmdprdsplit2  20143  ablfaclem3  20184  prdsmgp  20252  unitgrp  20491  subdrgint  20936  crng2idl  21450  gsumfsum  21614  pzriprnglem6  21666  chrid  21705  znleval  21734  frgpcyg  21753  ofldchr  21756  ocv1  21859  frlmip  21958  ellspd  21982  psrass1lem  22113  evlsvvval  22274  selvvvval  22323  ply1chr  22496  evl1var  22526  pf1mpf  22542  pf1ind  22545  mamuvs2  22593  madurid  22831  baspartn  23141  mretopd  23279  ordtcld1  23384  ordtcld2  23385  leordtvallem1  23397  leordtvallem2  23398  paste  23481  imacmp  23584  cmpsub  23587  unconn  23616  1stckgen  23741  ptbasfi  23768  txcld  23790  ptclsg  23802  txdis1cn  23822  ptrescn  23826  hausdiag  23832  txkgen  23839  xkoptsub  23841  xkococnlem  23846  cnmpt21  23858  cnmpt22  23861  tgqtop  23899  qtoprest  23904  kqdisj  23919  hmeores  23958  hmphindis  23984  pt1hmeo  23993  ptuncnv  23994  ptunhmeo  23995  xpstopnlem1  23996  xkohmeo  24002  alexsublem  24231  ptcmplem2  24240  tmdcn2  24276  cldsubg  24298  qustgplem  24308  tsmsres  24331  ustbas2  24412  ressuss  24449  metreslem  24549  xpsdsval  24568  prdsxmslem2  24716  txmetcnp  24734  tngngp  24841  nrmtngdist  24844  remetdval  24976  cnheibor  25144  evth2  25149  pcoass  25213  ncvspi  25345  iscmet3  25482  rrxip  25579  minveclem2  25615  cmmbl  25723  nulmbl2  25725  volinun  25735  voliunlem1  25739  volsup  25745  ovolioo  25757  uniiccdif  25767  uniioombllem2  25772  uniioombllem3  25774  uniioombllem4  25775  uniioombllem5  25776  ismbf3d  25843  itg2uba  25932  itg2i1fseq  25944  itgsplitioo  26027  limcflf  26070  cnplimc  26076  limcun  26084  dvfval  26086  dvres  26100  dvres3a  26103  dvnp1  26114  dvn1  26115  dvexp3  26167  dvsincos  26170  mvth  26181  c1lip2  26187  dvfsumlem2  26216  itgsubstlem  26237  itgsubst  26238  coeeq2  26429  dgreq0  26452  dgrcolem2  26461  vieta1  26503  ulm2  26578  radcnv0  26609  abelthlem2  26625  tanarg  26814  advlogexp  26850  efopn  26853  logtayl  26855  cxpcn3  26943  ang180lem3  27006  quad2  27034  mcubic  27042  binom4  27045  dquart  27048  quart1lem  27050  quart1  27051  quartlem1  27052  asinlem3a  27065  efiatan  27107  tanatan  27114  atanbndlem  27120  dvatan  27130  wilthlem2  27263  ftalem3  27269  ftalem5  27271  basellem3  27277  mumullem2  27374  musum  27385  mpodvdsmulf1o  27388  ppiub  27398  chtublem  27405  perfectlem2  27424  bposlem6  27483  bposlem9  27486  1lgs  27534  lgs1  27535  lgseisenlem1  27569  lgseisenlem2  27570  lgseisenlem3  27571  lgsquadlem2  27575  lgsquad2lem2  27579  2sqblem  27625  rpvmasum2  27706  log2sumbnd  27738  noetasuplem4  27930  ltslpss  28131  leslss  28132  bdayfinbndlem1  28690  z12shalf  28703  opphllem3  29060  prlngpln3  29229  vtxdun  29861  clwwlknon2num  30486  eucrct2eupth  30626  ex-fpar  30843  nvpi  31049  nvop  31058  phop  31200  minvecolem2  31257  hi01  31478  pjchi  31814  chjidm  31902  mayete3i  32110  ho0val  32132  lnop0  32348  adjbdlnb  32466  pjin2i  32575  mdslmd3i  32714  mdexchi  32717  imadifxp  32976  fcoinver  32979  suppovss  33056  fressupp  33063  supppreima  33066  mptprop  33073  f1od2  33094  fcobijfs  33096  ffsrn  33103  iocinif  33156  difioo  33157  indf1ofs  33216  cshw1s2  33304  gsummpt2co  33392  gsumhashmul  33411  gsummulsubdishift1s  33414  gsummulsubdishift2s  33415  symgfcoeu  33426  symgcom  33427  pmtrprfv2  33432  pmtrcnel2  33434  tocyc01  33462  cycpmconjv  33486  cycpmconjs  33500  elrgspnlem2  33587  lsmsnorb2  33729  krull  33785  opprqusbas  33794  opprqusplusg  33795  qsdrngi  33801  psrgsum  33962  psrmonprod  33966  ply1degltdimlem  34036  lindsun  34039  dimkerim  34041  fldexttr  34072  constrcon  34188  cos9thpiminplylem3  34198  smatlem  34211  zarcmplem  34295  esumpad2  34470  hasheuni  34499  esumcvg2  34501  esum2dlem  34506  sigapildsys  34576  measxun2  34624  measunl  34630  measinblem  34634  carsgclctunlem1  34731  carsgclctunlem3  34734  sibfof  34754  sitgclg  34756  eulerpartlemgf  34793  probdif  34834  cndprobval  34847  ballotlemic  34921  signsvtn0  34981  signstres  34986  chtvalz  35040  hgt750lemd  35059  bnj1415  35450  revwlk  35630  subfacp1lem1  35684  subfacp1lem3  35687  subfacp1lem5  35689  cvmscld  35778  cvmlift2lem9a  35808  cvmlift2lem9  35816  fwddifnp1  36670  dfttc4  37074  finxpreclem5  38074  ptrest  38303  poimirlem2  38306  poimirlem3  38307  poimirlem6  38310  poimirlem7  38311  poimirlem9  38313  poimirlem11  38315  poimirlem12  38316  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem24  38328  poimirlem25  38329  poimirlem27  38331  poimirlem28  38332  poimirlem29  38333  poimirlem31  38335  voliunnfl  38348  volsupnfl  38349  mbfresfi  38350  itg2addnclem2  38356  itg2addnclem3  38357  ftc1anclem5  38381  dvacos  38389  areacirclem5  38396  cocnv  38409  istotbnd3  38455  ssbnd  38472  disjresdisj  38926  eccnvepres3  38974  dfblockliftmap2  39143  symrelim  39325  osumcllem9N  40771  4atexlemex2  40878  cdleme20j  41125  cdlemg47  41543  diaintclN  41865  dibintclN  41974  dihintcl  42151  lclkrlem2e  42318  lclkrlem2p  42329  lcfrlem31  42380  lcmineqlem  42852  sticksstones8  42953  dvun  43153  readdlid  43197  fsuppssind  43358  prjspnval2  43383  flt4lem  43410  diophin  43536  monotuz  43701  monotoddzzfi  43702  oddcomabszz  43704  fnwe2val  43809  lnmlmic  43848  fiuneneq  43952  cytpval  43962  oaun3  44142  ntrkbimka  44797  ntrneifv2  44839  mnringmulrd  44980  mnringmulrcld  44985  radcnvrat  45057  nzprmdif  45062  binomcxplemnotnn0  45099  limsupvaluz  46455  ioccncflimc  46632  icocncflimc  46636  stoweidlem50  46797  fourierdlem48  46901  fourierdlem49  46902  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem107  46960  lambert0  47657  lamberte  47658  elsprel  48257  reuopreuprim  48308  perfectALTVlem2  48520  dfnbgr6  48655  dfsclnbgr6  48656  smprngprmrng  49137  restclssep  49727  seposep  49737  iscnrm3rlem8  49758  swapfid  50090  cofuswapf1  50105  cofuswapf2  50106  idfudiag1lem  50334  termcfuncval  50343  ranval  50431  lmddu  50478  initocmd  50480  logb2aval  50575  aacllem  50654