Theorem eqtr3id 2793

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  3eqtr3g  2802  csbeq1a  3842  ss2abdv  3993  ssdifeq0  4414  pofun  5512  opabbi2dv  5747  cnvsng  6115  csbpredg  6197  funcnvpr  6480  funcnvtp  6481  funcnvqp  6482  fresin  6627  fresaunres2  6630  f1imacnv  6716  foimacnv  6717  funfv  6837  dffv2  6845  fimacnvinrn  6931  rescnvimafod  6933  fsn2  6990  funiunfvf  7104  fcof1oinvd  7145  riotaxfrd  7247  f1opw2  7502  fnexALT  7767  fparlem3  7925  fparlem4  7926  fsplitfpar  7930  fvproj  7946  mpocurryd  8056  seqomlem1  8251  seqomlem4  8254  oasuc  8316  oesuclem  8317  omsuc  8318  onasuc  8320  onmsuc  8321  eqerlem  8490  pmresg  8616  fopwdom  8820  sbthlem8  8830  sbthlem9  8831  fodomr  8864  domss2  8872  mapen  8877  cnvfi  8924  enp1i  8982  xpfi  9015  fiint  9021  f1opwfi  9053  mapfien  9097  marypha1lem  9122  unxpwdom  9278  cantnfval2  9357  infxpenlem  9700  djuinf  9875  isf34lem3  10062  isf34lem5  10065  axdc4lem  10142  ttukeylem6  10201  rankcf  10464  tskuni  10470  gruima  10489  dmrecnq  10655  ltexnq  10662  reclem3pr  10736  pn0sr  10788  mulgt0sr  10792  recdiv  11611  2resupmax  12851  max0sub  12859  rexmul  12934  xmulmnf1  12939  xmulm1  12944  prunioo  13142  fseq1p1m1  13259  fzshftral  13273  seqp1d  13666  seqf1olem2  13691  seqfeq4  13700  binom3  13867  expmulnbnd  13878  discr  13883  bcn2  13961  hashun2  14026  hashun3  14027  hashdif  14056  hashgt12el  14065  hashgt12el2  14066  hashfacen  14094  hashfacenOLD  14095  s2prop  14548  s4prop  14551  s3sndisj  14606  s3iunsndisj  14607  cnrecnv  14804  rddif  14980  amgm2  15009  rlimres  15195  lo1res  15196  iseraltlem2  15322  iseralt  15324  fsumss  15365  fsumcl2lem  15371  isumclim3  15399  fsumcnv  15413  telfsumo  15442  fsumiun  15461  arisum2  15501  geoisum1c  15520  fprodss  15586  fprodser  15587  fprodcl2lem  15588  fprodsplit  15604  fprodn0  15617  fprodcnv  15621  iprodclim3  15638  risefac1  15671  fallfac1  15672  bpolyval  15687  bpoly3  15696  bpoly4  15697  fsumcube  15698  sinhval  15791  cos01bnd  15823  ruclem6  15872  sadadd2lem2  16085  eucalgval  16215  pcid  16502  prmreclem4  16548  4sqlem15  16588  4sqlem16  16589  ramcl  16658  strfv2d  16831  setsid  16837  imasvscafn  17165  xpsff1o  17195  xpsaddlem  17201  xpsvsca  17205  xpsle  17207  mreexexlem2d  17271  mreexexlem4d  17273  sscres  17452  xpcid  17822  evlfcllem  17855  hofcl  17893  isacs5lem  18178  frmdup3lem  18420  cayleylem2  18936  f1omvdco2  18971  symggen  18993  psgnunilem1  19016  pgp0  19116  sylow3lem2  19148  lsmdisjr  19205  lsmdisj2r  19206  subgdisj2  19213  efgval  19238  frgpuplem  19293  frgpup2  19297  gsumval3  19423  gsumzres  19425  gsum2d2lem  19489  dprdf1  19551  dmdprdsplit2lem  19563  dmdprdsplit2  19564  ablfaclem3  19605  prdsmgp  19764  unitgrp  19824  subdrgint  19986  crng2idl  20423  gsumfsum  20577  chrid  20643  znleval  20674  frgpcyg  20693  ocv1  20796  frlmip  20895  ellspd  20919  psrass1lemOLD  21053  psrass1lem  21056  evl1var  21412  pf1mpf  21428  pf1ind  21431  mamuvs2  21463  madurid  21701  baspartn  22012  mretopd  22151  ordtcld1  22256  ordtcld2  22257  leordtvallem1  22269  leordtvallem2  22270  paste  22353  imacmp  22456  cmpsub  22459  unconn  22488  1stckgen  22613  ptbasfi  22640  txcld  22662  ptclsg  22674  txdis1cn  22694  ptrescn  22698  hausdiag  22704  txkgen  22711  xkoptsub  22713  xkococnlem  22718  cnmpt21  22730  cnmpt22  22733  tgqtop  22771  qtoprest  22776  kqdisj  22791  hmeores  22830  hmphindis  22856  pt1hmeo  22865  ptuncnv  22866  ptunhmeo  22867  xpstopnlem1  22868  xkohmeo  22874  alexsublem  23103  ptcmplem2  23112  tmdcn2  23148  cldsubg  23170  qustgplem  23180  tsmsres  23203  ustbas2  23285  ressuss  23322  metreslem  23423  xpsdsval  23442  prdsxmslem2  23591  txmetcnp  23609  tngngp  23724  nrmtngdist  23727  remetdval  23858  cnheibor  24024  evth2  24029  pcoass  24093  ncvspi  24225  iscmet3  24362  rrxip  24459  minveclem2  24495  cmmbl  24603  nulmbl2  24605  volinun  24615  voliunlem1  24619  volsup  24625  ovolioo  24637  uniiccdif  24647  uniioombllem2  24652  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  ismbf3d  24723  itg2uba  24813  itg2i1fseq  24825  itgsplitioo  24907  limcflf  24950  cnplimc  24956  limcun  24964  dvfval  24966  dvres  24980  dvres3a  24983  dvnp1  24994  dvn1  24995  dvexp3  25047  dvsincos  25050  mvth  25061  c1lip2  25067  dvfsumlem2  25096  itgsubstlem  25117  itgsubst  25118  coeeq2  25308  dgreq0  25331  dgrcolem2  25340  vieta1  25377  ulm2  25449  radcnv0  25480  abelthlem2  25496  tanarg  25679  advlogexp  25715  efopn  25718  logtayl  25720  cxpcn3  25806  ang180lem3  25866  quad2  25894  mcubic  25902  binom4  25905  dquart  25908  quart1lem  25910  quart1  25911  quartlem1  25912  asinlem3a  25925  efiatan  25967  tanatan  25974  atanbndlem  25980  dvatan  25990  wilthlem2  26123  ftalem3  26129  ftalem5  26131  basellem3  26137  mumullem2  26234  musum  26245  chtublem  26264  perfectlem2  26283  bposlem6  26342  bposlem9  26345  1lgs  26393  lgs1  26394  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgsquadlem2  26434  lgsquad2lem2  26438  2sqblem  26484  rpvmasum2  26565  log2sumbnd  26597  opphllem3  27014  vtxdun  27751  clwwlknon2num  28370  eucrct2eupth  28510  ex-fpar  28727  nvpi  28930  nvop  28939  phop  29081  minvecolem2  29138  hi01  29359  pjchi  29695  chjidm  29783  mayete3i  29991  ho0val  30013  lnop0  30229  adjbdlnb  30347  pjin2i  30456  mdslmd3i  30595  mdexchi  30598  imadifxp  30841  fcoinver  30847  fnunres2  30917  suppovss  30919  fressupp  30924  supppreima  30927  mptprop  30933  padct  30956  f1od2  30958  fcobijfs  30960  ffsrn  30966  iocinif  31004  difioo  31005  s2rn  31120  s3rn  31122  cshw1s2  31134  gsummpt2co  31210  gsumhashmul  31218  symgfcoeu  31253  symgcom  31254  pmtrprfv2  31259  pmtrcnel2  31261  tocyc01  31287  cycpmconjv  31311  cycpmconjs  31325  ofldchr  31415  lsmsnorb2  31482  krull  31545  ply1chr  31571  rgmoddim  31595  lindsun  31608  dimkerim  31610  fldexttr  31635  smatlem  31649  zarcmplem  31733  indf1ofs  31894  esumpad2  31924  hasheuni  31953  esumcvg2  31955  esum2dlem  31960  sigapildsys  32030  measxun2  32078  measunl  32084  measinblem  32088  carsgclctunlem1  32184  carsgclctunlem3  32187  sibfof  32207  sitgclg  32209  eulerpartlemgf  32246  probdif  32287  cndprobval  32300  ballotlemic  32373  signsvtn0  32449  signstres  32454  chtvalz  32509  hgt750lemd  32528  bnj1415  32918  f1resrcmplf1d  32959  f1resfz0f1d  32972  revwlk  32986  subfacp1lem1  33041  subfacp1lem3  33044  subfacp1lem5  33046  cvmscld  33135  cvmlift2lem9a  33165  cvmlift2lem9  33173  ttrcltr  33702  noetasuplem4  33866  sltlpss  34014  fwddifnp1  34394  finxpreclem5  35493  ptrest  35703  poimirlem2  35706  poimirlem3  35707  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem24  35728  poimirlem25  35729  poimirlem27  35731  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  voliunnfl  35748  volsupnfl  35749  mbfresfi  35750  itg2addnclem2  35756  itg2addnclem3  35757  ftc1anclem5  35781  dvacos  35789  areacirclem5  35796  cocnv  35810  istotbnd3  35856  ssbnd  35873  eccnvepres3  36347  symrelim  36600  osumcllem9N  37905  4atexlemex2  38012  cdleme20j  38259  cdlemg47  38677  diaintclN  38999  dibintclN  39108  dihintcl  39285  lclkrlem2e  39452  lclkrlem2p  39463  lcfrlem31  39514  lcmineqlem  39988  sticksstones8  40037  evlsbagval  40198  fsuppssind  40205  readdid2  40307  prjspnval2  40378  flt4lem  40398  diophin  40510  monotuz  40679  monotoddzzfi  40680  oddcomabszz  40682  fnwe2val  40790  lnmlmic  40829  fiuneneq  40938  cytpval  40950  ntrkbimka  41537  ntrneifv2  41579  mnringmulrd  41728  mnringmulrcld  41735  radcnvrat  41821  nzprmdif  41826  binomcxplemnotnn0  41863  ioccncflimc  43316  icocncflimc  43320  stoweidlem50  43481  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem107  43644  elsprel  44815  reuopreuprim  44866  perfectALTVlem2  45062  restclssep  46097  seposep  46107  iscnrm3rlem8  46129  logb2aval  46352  aacllem  46391