Theorem eqtr3id 2788

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  3eqtr3g  2797  csbeq1a  3921  ssdifeq0  4492  pofun  5614  opabbi2dv  5862  cnvsng  6244  csbpredg  6328  funcnvpr  6629  funcnvtp  6630  funcnvqp  6631  fresin  6777  fresaunres2  6780  f1imacnv  6864  foimacnv  6865  funfv  6995  dffv2  7003  fimacnvinrn  7090  rescnvimafod  7092  fsn2  7155  funiunfvf  7268  fcof1oinvd  7312  riotaxfrd  7421  f1opw2  7687  fnexALT  7973  fparlem3  8137  fparlem4  8138  fsplitfpar  8141  fvproj  8157  mpocurryd  8292  seqomlem1  8488  seqomlem4  8491  oasuc  8560  oesuclem  8561  omsuc  8562  onasuc  8564  onmsuc  8565  eqerlem  8778  pmresg  8908  fopwdom  9118  sbthlem8  9128  sbthlem9  9129  fodomr  9166  domss2  9174  mapen  9179  cnvfi  9214  enp1iOLD  9311  xpfiOLD  9356  fiint  9363  fiintOLD  9364  fodomfir  9365  f1opwfi  9393  mapfien  9445  marypha1lem  9470  unxpwdom  9626  cantnfval2  9706  ttrcltr  9753  infxpenlem  10050  djuinf  10226  isf34lem3  10412  isf34lem5  10415  axdc4lem  10492  ttukeylem6  10551  rankcf  10814  tskuni  10820  gruima  10839  dmrecnq  11005  ltexnq  11012  reclem3pr  11086  pn0sr  11138  mulgt0sr  11142  recdiv  11970  2resupmax  13226  max0sub  13234  rexmul  13309  xmulmnf1  13314  xmulm1  13319  prunioo  13517  fseq1p1m1  13634  fzshftral  13651  seqp1d  14055  seqf1olem2  14079  seqfeq4  14088  binom3  14259  expmulnbnd  14270  discr  14275  bcn2  14354  hashun2  14418  hashun3  14419  hashdif  14448  hashgt12el  14457  hashgt12el2  14458  hashfacen  14489  s2prop  14942  s4prop  14945  s3sndisj  15002  s3iunsndisj  15003  cnrecnv  15200  rddif  15375  amgm2  15404  rlimres  15590  lo1res  15591  iseraltlem2  15715  iseralt  15717  fsumss  15757  fsumcl2lem  15763  isumclim3  15791  fsumcnv  15805  telfsumo  15834  fsumiun  15853  arisum2  15893  geoisum1c  15912  fprodss  15980  fprodser  15981  fprodcl2lem  15982  fprodsplit  15998  fprodn0  16011  fprodcnv  16015  iprodclim3  16032  risefac1  16065  fallfac1  16066  bpolyval  16081  bpoly3  16090  bpoly4  16091  fsumcube  16092  sinhval  16186  cos01bnd  16218  ruclem6  16267  sadadd2lem2  16483  eucalgval  16615  pcid  16906  prmreclem4  16952  4sqlem15  16992  4sqlem16  16993  ramcl  17062  strfv2d  17235  setsid  17241  imasvscafn  17583  xpsff1o  17613  xpsaddlem  17619  xpsvsca  17623  xpsle  17625  mreexexlem2d  17689  mreexexlem4d  17691  sscres  17870  xpcid  18244  evlfcllem  18277  hofcl  18315  isacs5lem  18602  frmdup3lem  18891  cayleylem2  19445  f1omvdco2  19480  symggen  19502  psgnunilem1  19525  pgp0  19628  sylow3lem2  19660  lsmdisjr  19716  lsmdisj2r  19717  subgdisj2  19724  efgval  19749  frgpuplem  19804  frgpup2  19808  gsumval3  19939  gsumzres  19941  gsum2d2lem  20005  dprdf1  20067  dmdprdsplit2lem  20079  dmdprdsplit2  20080  ablfaclem3  20121  prdsmgp  20168  unitgrp  20399  subdrgint  20820  crng2idl  21308  gsumfsum  21469  pzriprnglem6  21514  chrid  21557  znleval  21590  frgpcyg  21609  ocv1  21714  frlmip  21815  ellspd  21839  psrass1lem  21969  ply1chr  22325  evl1var  22355  pf1mpf  22371  pf1ind  22374  mamuvs2  22425  madurid  22665  baspartn  22976  mretopd  23115  ordtcld1  23220  ordtcld2  23221  leordtvallem1  23233  leordtvallem2  23234  paste  23317  imacmp  23420  cmpsub  23423  unconn  23452  1stckgen  23577  ptbasfi  23604  txcld  23626  ptclsg  23638  txdis1cn  23658  ptrescn  23662  hausdiag  23668  txkgen  23675  xkoptsub  23677  xkococnlem  23682  cnmpt21  23694  cnmpt22  23697  tgqtop  23735  qtoprest  23740  kqdisj  23755  hmeores  23794  hmphindis  23820  pt1hmeo  23829  ptuncnv  23830  ptunhmeo  23831  xpstopnlem1  23832  xkohmeo  23838  alexsublem  24067  ptcmplem2  24076  tmdcn2  24112  cldsubg  24134  qustgplem  24144  tsmsres  24167  ustbas2  24249  ressuss  24286  metreslem  24387  xpsdsval  24406  prdsxmslem2  24557  txmetcnp  24575  tngngp  24690  nrmtngdist  24693  remetdval  24824  cnheibor  25000  evth2  25005  pcoass  25070  ncvspi  25203  iscmet3  25340  rrxip  25437  minveclem2  25473  cmmbl  25582  nulmbl2  25584  volinun  25594  voliunlem1  25598  volsup  25604  ovolioo  25616  uniiccdif  25626  uniioombllem2  25631  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  ismbf3d  25702  itg2uba  25792  itg2i1fseq  25804  itgsplitioo  25887  limcflf  25930  cnplimc  25936  limcun  25944  dvfval  25946  dvres  25960  dvres3a  25963  dvnp1  25975  dvn1  25976  dvexp3  26030  dvsincos  26033  mvth  26045  c1lip2  26051  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgsubstlem  26103  itgsubst  26104  coeeq2  26295  dgreq0  26319  dgrcolem2  26328  vieta1  26368  ulm2  26442  radcnv0  26473  abelthlem2  26490  tanarg  26675  advlogexp  26711  efopn  26714  logtayl  26716  cxpcn3  26805  ang180lem3  26868  quad2  26896  mcubic  26904  binom4  26907  dquart  26910  quart1lem  26912  quart1  26913  quartlem1  26914  asinlem3a  26927  efiatan  26969  tanatan  26976  atanbndlem  26982  dvatan  26992  wilthlem2  27126  ftalem3  27132  ftalem5  27134  basellem3  27140  mumullem2  27237  musum  27248  mpodvdsmulf1o  27251  chtublem  27269  perfectlem2  27288  bposlem6  27347  bposlem9  27350  1lgs  27398  lgs1  27399  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgsquadlem2  27439  lgsquad2lem2  27443  2sqblem  27489  rpvmasum2  27570  log2sumbnd  27602  noetasuplem4  27795  sltlpss  27959  slelss  27960  opphllem3  28771  vtxdun  29513  clwwlknon2num  30133  eucrct2eupth  30273  ex-fpar  30490  nvpi  30695  nvop  30704  phop  30846  minvecolem2  30903  hi01  31124  pjchi  31460  chjidm  31548  mayete3i  31756  ho0val  31778  lnop0  31994  adjbdlnb  32112  pjin2i  32221  mdslmd3i  32360  mdexchi  32363  imadifxp  32620  fcoinver  32623  suppovss  32695  fressupp  32702  supppreima  32705  mptprop  32712  padct  32736  f1od2  32738  fcobijfs  32740  ffsrn  32746  iocinif  32789  difioo  32790  s2rnOLD  32912  s3rnOLD  32914  cshw1s2  32929  gsummpt2co  33033  gsumhashmul  33046  symgfcoeu  33084  symgcom  33085  pmtrprfv2  33090  pmtrcnel2  33092  tocyc01  33120  cycpmconjv  33144  cycpmconjs  33158  elrgspnlem2  33232  ofldchr  33323  lsmsnorb2  33399  krull  33486  opprqusbas  33495  opprqusplusg  33496  qsdrngi  33502  rgmoddimOLD  33637  ply1degltdimlem  33649  lindsun  33652  dimkerim  33654  fldexttr  33685  smatlem  33757  zarcmplem  33841  indf1ofs  34006  esumpad2  34036  hasheuni  34065  esumcvg2  34067  esum2dlem  34072  sigapildsys  34142  measxun2  34190  measunl  34196  measinblem  34200  carsgclctunlem1  34298  carsgclctunlem3  34301  sibfof  34321  sitgclg  34323  eulerpartlemgf  34360  probdif  34401  cndprobval  34414  ballotlemic  34487  signsvtn0  34563  signstres  34568  chtvalz  34622  hgt750lemd  34641  bnj1415  35030  f1resrcmplf1d  35079  f1resfz0f1d  35097  revwlk  35108  subfacp1lem1  35163  subfacp1lem3  35166  subfacp1lem5  35168  cvmscld  35257  cvmlift2lem9a  35287  cvmlift2lem9  35295  fwddifnp1  36146  finxpreclem5  37377  ptrest  37605  poimirlem2  37608  poimirlem3  37609  poimirlem6  37612  poimirlem7  37613  poimirlem9  37615  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  poimirlem25  37631  poimirlem27  37633  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  voliunnfl  37650  volsupnfl  37651  mbfresfi  37652  itg2addnclem2  37658  itg2addnclem3  37659  ftc1anclem5  37683  dvacos  37691  areacirclem5  37698  cocnv  37711  istotbnd3  37757  ssbnd  37774  disjresdisj  38221  eccnvepres3  38267  symrelim  38540  osumcllem9N  39946  4atexlemex2  40053  cdleme20j  40300  cdlemg47  40718  diaintclN  41040  dibintclN  41149  dihintcl  41326  lclkrlem2e  41493  lclkrlem2p  41504  lcfrlem31  41555  lcmineqlem  42033  sticksstones8  42134  dvun  42367  readdlid  42409  evlsvvval  42549  selvvvval  42571  fsuppssind  42579  prjspnval2  42604  flt4lem  42631  diophin  42759  monotuz  42929  monotoddzzfi  42930  oddcomabszz  42932  fnwe2val  43037  lnmlmic  43076  fiuneneq  43180  cytpval  43190  oaun3  43371  ntrkbimka  44027  ntrneifv2  44069  mnringmulrd  44216  mnringmulrcld  44223  radcnvrat  44309  nzprmdif  44314  binomcxplemnotnn0  44351  ioccncflimc  45840  icocncflimc  45844  stoweidlem50  46005  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem107  46168  elsprel  47399  reuopreuprim  47450  perfectALTVlem2  47646  dfnbgr6  47780  dfsclnbgr6  47781  restclssep  48711  seposep  48721  iscnrm3rlem8  48743  logb2aval  48994  aacllem  49031