Theorem eqtr3id 2786

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  3eqtr3g  2795  csbeq1a  3852  ssdifeq0  4427  pofun  5550  opabbi2dv  5798  cnvsng  6181  csbpredg  6265  funcnvpr  6554  funcnvtp  6555  funcnvqp  6556  f1imadifssran  6578  fresin  6703  fresaunres2  6706  f1imacnv  6790  foimacnv  6791  funfv  6921  dffv2  6929  fimacnvinrn  7017  rescnvimafod  7019  fsn2  7083  funiunfvf  7197  fcof1oinvd  7241  riotaxfrd  7351  f1opw2  7615  fnexALT  7897  fparlem3  8057  fparlem4  8058  fsplitfpar  8061  fvproj  8077  mpocurryd  8212  seqomlem1  8382  seqomlem4  8385  oasuc  8452  oesuclem  8453  omsuc  8454  onasuc  8456  onmsuc  8457  eqerlem  8672  pmresg  8811  fopwdom  9016  sbthlem8  9025  sbthlem9  9026  fodomr  9059  domss2  9067  mapen  9072  cnvfi  9103  fiint  9230  fodomfir  9231  f1opwfi  9259  mapfien  9314  marypha1lem  9339  unxpwdom  9497  cantnfval2  9581  ttrcltr  9628  infxpenlem  9926  djuinf  10102  isf34lem3  10288  isf34lem5  10291  axdc4lem  10368  ttukeylem6  10427  rankcf  10691  tskuni  10697  gruima  10716  dmrecnq  10882  ltexnq  10889  reclem3pr  10963  pn0sr  11015  mulgt0sr  11019  recdiv  11852  2resupmax  13131  max0sub  13139  rexmul  13214  xmulmnf1  13219  xmulm1  13224  prunioo  13425  fseq1p1m1  13543  fzshftral  13560  seqp1d  13971  seqf1olem2  13995  seqfeq4  14004  binom3  14177  expmulnbnd  14188  discr  14193  bcn2  14272  hashun2  14336  hashun3  14337  hashdif  14366  hashgt12el  14375  hashgt12el2  14376  hashfacen  14407  s2prop  14860  s4prop  14863  s3sndisj  14920  s3iunsndisj  14921  cnrecnv  15118  rddif  15294  amgm2  15323  rlimres  15511  lo1res  15512  iseraltlem2  15636  iseralt  15638  fsumss  15678  fsumcl2lem  15684  isumclim3  15712  fsumcnv  15726  telfsumo  15756  fsumiun  15775  arisum2  15817  geoisum1c  15836  fprodss  15904  fprodser  15905  fprodcl2lem  15906  fprodsplit  15922  fprodn0  15935  fprodcnv  15939  iprodclim3  15956  risefac1  15989  fallfac1  15990  bpolyval  16005  bpoly3  16014  bpoly4  16015  fsumcube  16016  sinhval  16112  cos01bnd  16144  ruclem6  16193  sadadd2lem2  16410  eucalgval  16542  pcid  16835  prmreclem4  16881  4sqlem15  16921  4sqlem16  16922  ramcl  16991  strfv2d  17162  setsid  17168  imasvscafn  17492  xpsff1o  17522  xpsaddlem  17528  xpsvsca  17532  xpsle  17534  mreexexlem2d  17602  mreexexlem4d  17604  sscres  17781  xpcid  18146  evlfcllem  18178  hofcl  18216  isacs5lem  18502  frmdup3lem  18825  cayleylem2  19379  f1omvdco2  19414  symggen  19436  psgnunilem1  19459  pgp0  19562  sylow3lem2  19594  lsmdisjr  19650  lsmdisj2r  19651  subgdisj2  19658  efgval  19683  frgpuplem  19738  frgpup2  19742  gsumval3  19873  gsumzres  19875  gsum2d2lem  19939  dprdf1  20001  dmdprdsplit2lem  20013  dmdprdsplit2  20014  ablfaclem3  20055  prdsmgp  20123  unitgrp  20354  subdrgint  20771  crng2idl  21271  gsumfsum  21424  pzriprnglem6  21476  chrid  21515  znleval  21544  frgpcyg  21563  ofldchr  21566  ocv1  21669  frlmip  21768  ellspd  21792  psrass1lem  21922  evlsvvval  22081  ply1chr  22281  evl1var  22311  pf1mpf  22327  pf1ind  22330  mamuvs2  22381  madurid  22619  baspartn  22929  mretopd  23067  ordtcld1  23172  ordtcld2  23173  leordtvallem1  23185  leordtvallem2  23186  paste  23269  imacmp  23372  cmpsub  23375  unconn  23404  1stckgen  23529  ptbasfi  23556  txcld  23578  ptclsg  23590  txdis1cn  23610  ptrescn  23614  hausdiag  23620  txkgen  23627  xkoptsub  23629  xkococnlem  23634  cnmpt21  23646  cnmpt22  23649  tgqtop  23687  qtoprest  23692  kqdisj  23707  hmeores  23746  hmphindis  23772  pt1hmeo  23781  ptuncnv  23782  ptunhmeo  23783  xpstopnlem1  23784  xkohmeo  23790  alexsublem  24019  ptcmplem2  24028  tmdcn2  24064  cldsubg  24086  qustgplem  24096  tsmsres  24119  ustbas2  24200  ressuss  24237  metreslem  24337  xpsdsval  24356  prdsxmslem2  24504  txmetcnp  24522  tngngp  24629  nrmtngdist  24632  remetdval  24764  cnheibor  24932  evth2  24937  pcoass  25001  ncvspi  25133  iscmet3  25270  rrxip  25367  minveclem2  25403  cmmbl  25511  nulmbl2  25513  volinun  25523  voliunlem1  25527  volsup  25533  ovolioo  25545  uniiccdif  25555  uniioombllem2  25560  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  ismbf3d  25631  itg2uba  25720  itg2i1fseq  25732  itgsplitioo  25815  limcflf  25858  cnplimc  25864  limcun  25872  dvfval  25874  dvres  25888  dvres3a  25891  dvnp1  25902  dvn1  25903  dvexp3  25955  dvsincos  25958  mvth  25969  c1lip2  25975  dvfsumlem2  26004  itgsubstlem  26025  itgsubst  26026  coeeq2  26217  dgreq0  26240  dgrcolem2  26249  vieta1  26289  ulm2  26363  radcnv0  26394  abelthlem2  26410  tanarg  26596  advlogexp  26632  efopn  26635  logtayl  26637  cxpcn3  26725  ang180lem3  26788  quad2  26816  mcubic  26824  binom4  26827  dquart  26830  quart1lem  26832  quart1  26833  quartlem1  26834  asinlem3a  26847  efiatan  26889  tanatan  26896  atanbndlem  26902  dvatan  26912  wilthlem2  27046  ftalem3  27052  ftalem5  27054  basellem3  27060  mumullem2  27157  musum  27168  mpodvdsmulf1o  27171  chtublem  27188  perfectlem2  27207  bposlem6  27266  bposlem9  27269  1lgs  27317  lgs1  27318  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgsquadlem2  27358  lgsquad2lem2  27362  2sqblem  27408  rpvmasum2  27489  log2sumbnd  27521  noetasuplem4  27714  ltslpss  27914  leslss  27915  bdayfinbndlem1  28473  z12shalf  28486  opphllem3  28831  vtxdun  29565  clwwlknon2num  30190  eucrct2eupth  30330  ex-fpar  30547  nvpi  30753  nvop  30762  phop  30904  minvecolem2  30961  hi01  31182  pjchi  31518  chjidm  31606  mayete3i  31814  ho0val  31836  lnop0  32052  adjbdlnb  32170  pjin2i  32279  mdslmd3i  32418  mdexchi  32421  imadifxp  32686  fcoinver  32689  suppovss  32769  fressupp  32776  supppreima  32779  mptprop  32786  f1od2  32807  fcobijfs  32809  ffsrn  32816  iocinif  32869  difioo  32870  indf1ofs  32941  s2rnOLD  33019  s3rnOLD  33021  cshw1s2  33035  gsummpt2co  33124  gsumhashmul  33143  gsummulsubdishift1s  33146  gsummulsubdishift2s  33147  symgfcoeu  33158  symgcom  33159  pmtrprfv2  33164  pmtrcnel2  33166  tocyc01  33194  cycpmconjv  33218  cycpmconjs  33232  elrgspnlem2  33319  lsmsnorb2  33467  krull  33554  opprqusbas  33563  opprqusplusg  33564  qsdrngi  33570  psrgsum  33707  psrmonprod  33711  rgmoddimOLD  33770  ply1degltdimlem  33782  lindsun  33785  dimkerim  33787  fldexttr  33818  constrcon  33934  cos9thpiminplylem3  33944  smatlem  33957  zarcmplem  34041  esumpad2  34216  hasheuni  34245  esumcvg2  34247  esum2dlem  34252  sigapildsys  34322  measxun2  34370  measunl  34376  measinblem  34380  carsgclctunlem1  34477  carsgclctunlem3  34480  sibfof  34500  sitgclg  34502  eulerpartlemgf  34539  probdif  34580  cndprobval  34593  ballotlemic  34667  signsvtn0  34730  signstres  34735  chtvalz  34789  hgt750lemd  34808  bnj1415  35196  f1resrcmplf1d  35246  f1resfz0f1d  35312  revwlk  35323  subfacp1lem1  35377  subfacp1lem3  35380  subfacp1lem5  35382  cvmscld  35471  cvmlift2lem9a  35501  cvmlift2lem9  35509  fwddifnp1  36363  dfttc4  36728  finxpreclem5  37725  ptrest  37954  poimirlem2  37957  poimirlem3  37958  poimirlem6  37961  poimirlem7  37962  poimirlem9  37964  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem24  37979  poimirlem25  37980  poimirlem27  37982  poimirlem28  37983  poimirlem29  37984  poimirlem31  37986  voliunnfl  37999  volsupnfl  38000  mbfresfi  38001  itg2addnclem2  38007  itg2addnclem3  38008  ftc1anclem5  38032  dvacos  38040  areacirclem5  38047  cocnv  38060  istotbnd3  38106  ssbnd  38123  disjresdisj  38579  eccnvepres3  38627  dfblockliftmap2  38796  symrelim  38978  osumcllem9N  40424  4atexlemex2  40531  cdleme20j  40778  cdlemg47  41196  diaintclN  41518  dibintclN  41627  dihintcl  41804  lclkrlem2e  41971  lclkrlem2p  41982  lcfrlem31  42033  lcmineqlem  42505  sticksstones8  42606  dvun  42805  readdlid  42849  selvvvval  43032  fsuppssind  43040  prjspnval2  43065  flt4lem  43092  diophin  43218  monotuz  43387  monotoddzzfi  43388  oddcomabszz  43390  fnwe2val  43495  lnmlmic  43534  fiuneneq  43638  cytpval  43648  oaun3  43828  ntrkbimka  44483  ntrneifv2  44525  mnringmulrd  44668  mnringmulrcld  44673  radcnvrat  44759  nzprmdif  44764  binomcxplemnotnn0  44801  ioccncflimc  46331  icocncflimc  46335  stoweidlem50  46496  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem107  46659  lambert0  47347  lamberte  47348  elsprel  47947  reuopreuprim  47998  perfectALTVlem2  48210  dfnbgr6  48345  dfsclnbgr6  48346  restclssep  49403  seposep  49413  iscnrm3rlem8  49434  swapfid  49766  cofuswapf1  49781  cofuswapf2  49782  idfudiag1lem  50010  termcfuncval  50019  ranval  50107  lmddu  50154  initocmd  50156  logb2aval  50251  aacllem  50288