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 2748	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2791	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  3eqtr3g  2802  csbeq1a  3847  ss2abdv  3998  ssdifeq0  4418  pofun  5522  opabbi2dv  5761  cnvsng  6131  csbpredg  6212  funcnvpr  6503  funcnvtp  6504  funcnvqp  6505  fresin  6652  fresaunres2  6655  f1imacnv  6741  foimacnv  6742  funfv  6864  dffv2  6872  fimacnvinrn  6958  rescnvimafod  6960  fsn2  7017  funiunfvf  7131  fcof1oinvd  7174  riotaxfrd  7276  f1opw2  7533  fnexALT  7802  fparlem3  7963  fparlem4  7964  fsplitfpar  7968  fvproj  7984  mpocurryd  8094  seqomlem1  8290  seqomlem4  8293  oasuc  8363  oesuclem  8364  omsuc  8365  onasuc  8367  onmsuc  8368  eqerlem  8541  pmresg  8667  fopwdom  8876  sbthlem8  8886  sbthlem9  8887  fodomr  8924  domss2  8932  mapen  8937  cnvfi  8972  enp1i  9061  xpfi  9094  fiint  9100  f1opwfi  9132  mapfien  9176  marypha1lem  9201  unxpwdom  9357  cantnfval2  9436  ttrcltr  9483  infxpenlem  9778  djuinf  9953  isf34lem3  10140  isf34lem5  10143  axdc4lem  10220  ttukeylem6  10279  rankcf  10542  tskuni  10548  gruima  10567  dmrecnq  10733  ltexnq  10740  reclem3pr  10814  pn0sr  10866  mulgt0sr  10870  recdiv  11690  2resupmax  12931  max0sub  12939  rexmul  13014  xmulmnf1  13019  xmulm1  13024  prunioo  13222  fseq1p1m1  13339  fzshftral  13353  seqp1d  13747  seqf1olem2  13772  seqfeq4  13781  binom3  13948  expmulnbnd  13959  discr  13964  bcn2  14042  hashun2  14107  hashun3  14108  hashdif  14137  hashgt12el  14146  hashgt12el2  14147  hashfacen  14175  hashfacenOLD  14176  s2prop  14629  s4prop  14632  s3sndisj  14687  s3iunsndisj  14688  cnrecnv  14885  rddif  15061  amgm2  15090  rlimres  15276  lo1res  15277  iseraltlem2  15403  iseralt  15405  fsumss  15446  fsumcl2lem  15452  isumclim3  15480  fsumcnv  15494  telfsumo  15523  fsumiun  15542  arisum2  15582  geoisum1c  15601  fprodss  15667  fprodser  15668  fprodcl2lem  15669  fprodsplit  15685  fprodn0  15698  fprodcnv  15702  iprodclim3  15719  risefac1  15752  fallfac1  15753  bpolyval  15768  bpoly3  15777  bpoly4  15778  fsumcube  15779  sinhval  15872  cos01bnd  15904  ruclem6  15953  sadadd2lem2  16166  eucalgval  16296  pcid  16583  prmreclem4  16629  4sqlem15  16669  4sqlem16  16670  ramcl  16739  strfv2d  16912  setsid  16918  imasvscafn  17257  xpsff1o  17287  xpsaddlem  17293  xpsvsca  17297  xpsle  17299  mreexexlem2d  17363  mreexexlem4d  17365  sscres  17544  xpcid  17915  evlfcllem  17948  hofcl  17986  isacs5lem  18272  frmdup3lem  18514  cayleylem2  19030  f1omvdco2  19065  symggen  19087  psgnunilem1  19110  pgp0  19210  sylow3lem2  19242  lsmdisjr  19299  lsmdisj2r  19300  subgdisj2  19307  efgval  19332  frgpuplem  19387  frgpup2  19391  gsumval3  19517  gsumzres  19519  gsum2d2lem  19583  dprdf1  19645  dmdprdsplit2lem  19657  dmdprdsplit2  19658  ablfaclem3  19699  prdsmgp  19858  unitgrp  19918  subdrgint  20080  crng2idl  20519  gsumfsum  20674  chrid  20740  znleval  20771  frgpcyg  20790  ocv1  20893  frlmip  20994  ellspd  21018  psrass1lemOLD  21152  psrass1lem  21155  evl1var  21511  pf1mpf  21527  pf1ind  21530  mamuvs2  21562  madurid  21802  baspartn  22113  mretopd  22252  ordtcld1  22357  ordtcld2  22358  leordtvallem1  22370  leordtvallem2  22371  paste  22454  imacmp  22557  cmpsub  22560  unconn  22589  1stckgen  22714  ptbasfi  22741  txcld  22763  ptclsg  22775  txdis1cn  22795  ptrescn  22799  hausdiag  22805  txkgen  22812  xkoptsub  22814  xkococnlem  22819  cnmpt21  22831  cnmpt22  22834  tgqtop  22872  qtoprest  22877  kqdisj  22892  hmeores  22931  hmphindis  22957  pt1hmeo  22966  ptuncnv  22967  ptunhmeo  22968  xpstopnlem1  22969  xkohmeo  22975  alexsublem  23204  ptcmplem2  23213  tmdcn2  23249  cldsubg  23271  qustgplem  23281  tsmsres  23304  ustbas2  23386  ressuss  23423  metreslem  23524  xpsdsval  23543  prdsxmslem2  23694  txmetcnp  23712  tngngp  23827  nrmtngdist  23830  remetdval  23961  cnheibor  24127  evth2  24132  pcoass  24196  ncvspi  24329  iscmet3  24466  rrxip  24563  minveclem2  24599  cmmbl  24707  nulmbl2  24709  volinun  24719  voliunlem1  24723  volsup  24729  ovolioo  24741  uniiccdif  24751  uniioombllem2  24756  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  ismbf3d  24827  itg2uba  24917  itg2i1fseq  24929  itgsplitioo  25011  limcflf  25054  cnplimc  25060  limcun  25068  dvfval  25070  dvres  25084  dvres3a  25087  dvnp1  25098  dvn1  25099  dvexp3  25151  dvsincos  25154  mvth  25165  c1lip2  25171  dvfsumlem2  25200  itgsubstlem  25221  itgsubst  25222  coeeq2  25412  dgreq0  25435  dgrcolem2  25444  vieta1  25481  ulm2  25553  radcnv0  25584  abelthlem2  25600  tanarg  25783  advlogexp  25819  efopn  25822  logtayl  25824  cxpcn3  25910  ang180lem3  25970  quad2  25998  mcubic  26006  binom4  26009  dquart  26012  quart1lem  26014  quart1  26015  quartlem1  26016  asinlem3a  26029  efiatan  26071  tanatan  26078  atanbndlem  26084  dvatan  26094  wilthlem2  26227  ftalem3  26233  ftalem5  26235  basellem3  26241  mumullem2  26338  musum  26349  chtublem  26368  perfectlem2  26387  bposlem6  26446  bposlem9  26449  1lgs  26497  lgs1  26498  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgsquadlem2  26538  lgsquad2lem2  26542  2sqblem  26588  rpvmasum2  26669  log2sumbnd  26701  opphllem3  27119  vtxdun  27857  clwwlknon2num  28478  eucrct2eupth  28618  ex-fpar  28835  nvpi  29038  nvop  29047  phop  29189  minvecolem2  29246  hi01  29467  pjchi  29803  chjidm  29891  mayete3i  30099  ho0val  30121  lnop0  30337  adjbdlnb  30455  pjin2i  30564  mdslmd3i  30703  mdexchi  30706  imadifxp  30949  fcoinver  30955  fnunres2  31024  suppovss  31026  fressupp  31031  supppreima  31034  mptprop  31040  padct  31063  f1od2  31065  fcobijfs  31067  ffsrn  31073  iocinif  31111  difioo  31112  s2rn  31227  s3rn  31229  cshw1s2  31241  gsummpt2co  31317  gsumhashmul  31325  symgfcoeu  31360  symgcom  31361  pmtrprfv2  31366  pmtrcnel2  31368  tocyc01  31394  cycpmconjv  31418  cycpmconjs  31432  ofldchr  31522  lsmsnorb2  31589  krull  31652  ply1chr  31678  rgmoddim  31702  lindsun  31715  dimkerim  31717  fldexttr  31742  smatlem  31756  zarcmplem  31840  indf1ofs  32003  esumpad2  32033  hasheuni  32062  esumcvg2  32064  esum2dlem  32069  sigapildsys  32139  measxun2  32187  measunl  32193  measinblem  32197  carsgclctunlem1  32293  carsgclctunlem3  32296  sibfof  32316  sitgclg  32318  eulerpartlemgf  32355  probdif  32396  cndprobval  32409  ballotlemic  32482  signsvtn0  32558  signstres  32563  chtvalz  32618  hgt750lemd  32637  bnj1415  33027  f1resrcmplf1d  33068  f1resfz0f1d  33081  revwlk  33095  subfacp1lem1  33150  subfacp1lem3  33153  subfacp1lem5  33155  cvmscld  33244  cvmlift2lem9a  33274  cvmlift2lem9  33282  noetasuplem4  33948  sltlpss  34096  fwddifnp1  34476  finxpreclem5  35575  ptrest  35785  poimirlem2  35788  poimirlem3  35789  poimirlem6  35792  poimirlem7  35793  poimirlem9  35795  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem24  35810  poimirlem25  35811  poimirlem27  35813  poimirlem28  35814  poimirlem29  35815  poimirlem31  35817  voliunnfl  35830  volsupnfl  35831  mbfresfi  35832  itg2addnclem2  35838  itg2addnclem3  35839  ftc1anclem5  35863  dvacos  35871  areacirclem5  35878  cocnv  35892  istotbnd3  35938  ssbnd  35955  eccnvepres3  36428  symrelim  36680  osumcllem9N  37985  4atexlemex2  38092  cdleme20j  38339  cdlemg47  38757  diaintclN  39079  dibintclN  39188  dihintcl  39365  lclkrlem2e  39532  lclkrlem2p  39543  lcfrlem31  39594  lcmineqlem  40067  sticksstones8  40116  evlsbagval  40282  fsuppssind  40289  readdid2  40393  prjspnval2  40464  flt4lem  40489  diophin  40601  monotuz  40770  monotoddzzfi  40771  oddcomabszz  40773  fnwe2val  40881  lnmlmic  40920  fiuneneq  41029  cytpval  41041  ntrkbimka  41655  ntrneifv2  41697  mnringmulrd  41846  mnringmulrcld  41853  radcnvrat  41939  nzprmdif  41944  binomcxplemnotnn0  41981  ioccncflimc  43433  icocncflimc  43437  stoweidlem50  43598  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem107  43761  elsprel  44938  reuopreuprim  44989  perfectALTVlem2  45185  restclssep  46220  seposep  46230  iscnrm3rlem8  46252  logb2aval  46477  aacllem  46516