Theorem eqtr3id 2778

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  3eqtr3g  2787  csbeq1a  3873  ssdifeq0  4446  pofun  5557  opabbi2dv  5803  cnvsng  6184  csbpredg  6268  funcnvpr  6562  funcnvtp  6563  funcnvqp  6564  f1imadifssran  6586  fresin  6711  fresaunres2  6714  f1imacnv  6798  foimacnv  6799  funfv  6930  dffv2  6938  fimacnvinrn  7025  rescnvimafod  7027  fsn2  7090  funiunfvf  7205  fcof1oinvd  7250  riotaxfrd  7360  f1opw2  7624  fnexALT  7909  fparlem3  8070  fparlem4  8071  fsplitfpar  8074  fvproj  8090  mpocurryd  8225  seqomlem1  8395  seqomlem4  8398  oasuc  8465  oesuclem  8466  omsuc  8467  onasuc  8469  onmsuc  8470  eqerlem  8683  pmresg  8820  fopwdom  9026  sbthlem8  9035  sbthlem9  9036  fodomr  9069  domss2  9077  mapen  9082  cnvfi  9117  enp1iOLD  9201  xpfiOLD  9246  fiint  9253  fiintOLD  9254  fodomfir  9255  f1opwfi  9283  mapfien  9335  marypha1lem  9360  unxpwdom  9518  cantnfval2  9598  ttrcltr  9645  infxpenlem  9942  djuinf  10118  isf34lem3  10304  isf34lem5  10307  axdc4lem  10384  ttukeylem6  10443  rankcf  10706  tskuni  10712  gruima  10731  dmrecnq  10897  ltexnq  10904  reclem3pr  10978  pn0sr  11030  mulgt0sr  11034  recdiv  11864  2resupmax  13124  max0sub  13132  rexmul  13207  xmulmnf1  13212  xmulm1  13217  prunioo  13418  fseq1p1m1  13535  fzshftral  13552  seqp1d  13959  seqf1olem2  13983  seqfeq4  13992  binom3  14165  expmulnbnd  14176  discr  14181  bcn2  14260  hashun2  14324  hashun3  14325  hashdif  14354  hashgt12el  14363  hashgt12el2  14364  hashfacen  14395  s2prop  14849  s4prop  14852  s3sndisj  14909  s3iunsndisj  14910  cnrecnv  15107  rddif  15283  amgm2  15312  rlimres  15500  lo1res  15501  iseraltlem2  15625  iseralt  15627  fsumss  15667  fsumcl2lem  15673  isumclim3  15701  fsumcnv  15715  telfsumo  15744  fsumiun  15763  arisum2  15803  geoisum1c  15822  fprodss  15890  fprodser  15891  fprodcl2lem  15892  fprodsplit  15908  fprodn0  15921  fprodcnv  15925  iprodclim3  15942  risefac1  15975  fallfac1  15976  bpolyval  15991  bpoly3  16000  bpoly4  16001  fsumcube  16002  sinhval  16098  cos01bnd  16130  ruclem6  16179  sadadd2lem2  16396  eucalgval  16528  pcid  16820  prmreclem4  16866  4sqlem15  16906  4sqlem16  16907  ramcl  16976  strfv2d  17147  setsid  17153  imasvscafn  17476  xpsff1o  17506  xpsaddlem  17512  xpsvsca  17516  xpsle  17518  mreexexlem2d  17582  mreexexlem4d  17584  sscres  17761  xpcid  18126  evlfcllem  18158  hofcl  18196  isacs5lem  18480  frmdup3lem  18769  cayleylem2  19319  f1omvdco2  19354  symggen  19376  psgnunilem1  19399  pgp0  19502  sylow3lem2  19534  lsmdisjr  19590  lsmdisj2r  19591  subgdisj2  19598  efgval  19623  frgpuplem  19678  frgpup2  19682  gsumval3  19813  gsumzres  19815  gsum2d2lem  19879  dprdf1  19941  dmdprdsplit2lem  19953  dmdprdsplit2  19954  ablfaclem3  19995  prdsmgp  20036  unitgrp  20268  subdrgint  20688  crng2idl  21167  gsumfsum  21327  pzriprnglem6  21372  chrid  21411  znleval  21440  frgpcyg  21459  ocv1  21564  frlmip  21663  ellspd  21687  psrass1lem  21817  ply1chr  22169  evl1var  22199  pf1mpf  22215  pf1ind  22218  mamuvs2  22269  madurid  22507  baspartn  22817  mretopd  22955  ordtcld1  23060  ordtcld2  23061  leordtvallem1  23073  leordtvallem2  23074  paste  23157  imacmp  23260  cmpsub  23263  unconn  23292  1stckgen  23417  ptbasfi  23444  txcld  23466  ptclsg  23478  txdis1cn  23498  ptrescn  23502  hausdiag  23508  txkgen  23515  xkoptsub  23517  xkococnlem  23522  cnmpt21  23534  cnmpt22  23537  tgqtop  23575  qtoprest  23580  kqdisj  23595  hmeores  23634  hmphindis  23660  pt1hmeo  23669  ptuncnv  23670  ptunhmeo  23671  xpstopnlem1  23672  xkohmeo  23678  alexsublem  23907  ptcmplem2  23916  tmdcn2  23952  cldsubg  23974  qustgplem  23984  tsmsres  24007  ustbas2  24089  ressuss  24126  metreslem  24226  xpsdsval  24245  prdsxmslem2  24393  txmetcnp  24411  tngngp  24518  nrmtngdist  24521  remetdval  24653  cnheibor  24830  evth2  24835  pcoass  24900  ncvspi  25032  iscmet3  25169  rrxip  25266  minveclem2  25302  cmmbl  25411  nulmbl2  25413  volinun  25423  voliunlem1  25427  volsup  25433  ovolioo  25445  uniiccdif  25455  uniioombllem2  25460  uniioombllem3  25462  uniioombllem4  25463  uniioombllem5  25464  ismbf3d  25531  itg2uba  25620  itg2i1fseq  25632  itgsplitioo  25715  limcflf  25758  cnplimc  25764  limcun  25772  dvfval  25774  dvres  25788  dvres3a  25791  dvnp1  25803  dvn1  25804  dvexp3  25858  dvsincos  25861  mvth  25873  c1lip2  25879  dvfsumlem2  25909  dvfsumlem2OLD  25910  itgsubstlem  25931  itgsubst  25932  coeeq2  26123  dgreq0  26147  dgrcolem2  26156  vieta1  26196  ulm2  26270  radcnv0  26301  abelthlem2  26318  tanarg  26504  advlogexp  26540  efopn  26543  logtayl  26545  cxpcn3  26634  ang180lem3  26697  quad2  26725  mcubic  26733  binom4  26736  dquart  26739  quart1lem  26741  quart1  26742  quartlem1  26743  asinlem3a  26756  efiatan  26798  tanatan  26805  atanbndlem  26811  dvatan  26821  wilthlem2  26955  ftalem3  26961  ftalem5  26963  basellem3  26969  mumullem2  27066  musum  27077  mpodvdsmulf1o  27080  chtublem  27098  perfectlem2  27117  bposlem6  27176  bposlem9  27179  1lgs  27227  lgs1  27228  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgsquadlem2  27268  lgsquad2lem2  27272  2sqblem  27318  rpvmasum2  27399  log2sumbnd  27431  noetasuplem4  27624  sltlpss  27795  slelss  27796  opphllem3  28652  vtxdun  29385  clwwlknon2num  30007  eucrct2eupth  30147  ex-fpar  30364  nvpi  30569  nvop  30578  phop  30720  minvecolem2  30777  hi01  30998  pjchi  31334  chjidm  31422  mayete3i  31630  ho0val  31652  lnop0  31868  adjbdlnb  31986  pjin2i  32095  mdslmd3i  32234  mdexchi  32237  imadifxp  32503  fcoinver  32506  suppovss  32577  fressupp  32584  supppreima  32587  mptprop  32594  padct  32616  f1od2  32617  fcobijfs  32619  ffsrn  32625  iocinif  32677  difioo  32678  indf1ofs  32762  s2rnOLD  32838  s3rnOLD  32840  cshw1s2  32855  gsummpt2co  32961  gsumhashmul  32974  symgfcoeu  33012  symgcom  33013  pmtrprfv2  33018  pmtrcnel2  33020  tocyc01  33048  cycpmconjv  33072  cycpmconjs  33086  elrgspnlem2  33167  ofldchr  33265  lsmsnorb2  33336  krull  33423  opprqusbas  33432  opprqusplusg  33433  qsdrngi  33439  rgmoddimOLD  33579  ply1degltdimlem  33591  lindsun  33594  dimkerim  33596  fldexttr  33627  constrcon  33737  cos9thpiminplylem3  33747  smatlem  33760  zarcmplem  33844  esumpad2  34019  hasheuni  34048  esumcvg2  34050  esum2dlem  34055  sigapildsys  34125  measxun2  34173  measunl  34179  measinblem  34183  carsgclctunlem1  34281  carsgclctunlem3  34284  sibfof  34304  sitgclg  34306  eulerpartlemgf  34343  probdif  34384  cndprobval  34397  ballotlemic  34471  signsvtn0  34534  signstres  34539  chtvalz  34593  hgt750lemd  34612  bnj1415  35001  f1resrcmplf1d  35050  f1resfz0f1d  35074  revwlk  35085  subfacp1lem1  35139  subfacp1lem3  35142  subfacp1lem5  35144  cvmscld  35233  cvmlift2lem9a  35263  cvmlift2lem9  35271  fwddifnp1  36126  finxpreclem5  37356  ptrest  37586  poimirlem2  37589  poimirlem3  37590  poimirlem6  37593  poimirlem7  37594  poimirlem9  37596  poimirlem11  37598  poimirlem12  37599  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem24  37611  poimirlem25  37612  poimirlem27  37614  poimirlem28  37615  poimirlem29  37616  poimirlem31  37618  voliunnfl  37631  volsupnfl  37632  mbfresfi  37633  itg2addnclem2  37639  itg2addnclem3  37640  ftc1anclem5  37664  dvacos  37672  areacirclem5  37679  cocnv  37692  istotbnd3  37738  ssbnd  37755  disjresdisj  38202  eccnvepres3  38247  symrelim  38523  osumcllem9N  39931  4atexlemex2  40038  cdleme20j  40285  cdlemg47  40703  diaintclN  41025  dibintclN  41134  dihintcl  41311  lclkrlem2e  41478  lclkrlem2p  41489  lcfrlem31  41540  lcmineqlem  42013  sticksstones8  42114  dvun  42320  readdlid  42364  evlsvvval  42524  selvvvval  42546  fsuppssind  42554  prjspnval2  42579  flt4lem  42606  diophin  42733  monotuz  42903  monotoddzzfi  42904  oddcomabszz  42906  fnwe2val  43011  lnmlmic  43050  fiuneneq  43154  cytpval  43164  oaun3  43344  ntrkbimka  44000  ntrneifv2  44042  mnringmulrd  44185  mnringmulrcld  44190  radcnvrat  44276  nzprmdif  44281  binomcxplemnotnn0  44318  ioccncflimc  45856  icocncflimc  45860  stoweidlem50  46021  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem107  46184  lambert0  46861  lamberte  46862  elsprel  47449  reuopreuprim  47500  perfectALTVlem2  47696  dfnbgr6  47830  dfsclnbgr6  47831  restclssep  48877  seposep  48887  iscnrm3rlem8  48908  swapfid  49241  cofuswapf1  49256  cofuswapf2  49257  idfudiag1lem  49485  termcfuncval  49494  ranval  49582  lmddu  49629  initocmd  49631  logb2aval  49726  aacllem  49763