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  3876  ssdifeq0  4450  pofun  5564  opabbi2dv  5813  cnvsng  6196  csbpredg  6280  funcnvpr  6578  funcnvtp  6579  funcnvqp  6580  f1imadifssran  6602  fresin  6729  fresaunres2  6732  f1imacnv  6816  foimacnv  6817  funfv  6948  dffv2  6956  fimacnvinrn  7043  rescnvimafod  7045  fsn2  7108  funiunfvf  7223  fcof1oinvd  7268  riotaxfrd  7378  f1opw2  7644  fnexALT  7929  fparlem3  8093  fparlem4  8094  fsplitfpar  8097  fvproj  8113  mpocurryd  8248  seqomlem1  8418  seqomlem4  8421  oasuc  8488  oesuclem  8489  omsuc  8490  onasuc  8492  onmsuc  8493  eqerlem  8706  pmresg  8843  fopwdom  9049  sbthlem8  9058  sbthlem9  9059  fodomr  9092  domss2  9100  mapen  9105  cnvfi  9140  enp1iOLD  9225  xpfiOLD  9270  fiint  9277  fiintOLD  9278  fodomfir  9279  f1opwfi  9307  mapfien  9359  marypha1lem  9384  unxpwdom  9542  cantnfval2  9622  ttrcltr  9669  infxpenlem  9966  djuinf  10142  isf34lem3  10328  isf34lem5  10331  axdc4lem  10408  ttukeylem6  10467  rankcf  10730  tskuni  10736  gruima  10755  dmrecnq  10921  ltexnq  10928  reclem3pr  11002  pn0sr  11054  mulgt0sr  11058  recdiv  11888  2resupmax  13148  max0sub  13156  rexmul  13231  xmulmnf1  13236  xmulm1  13241  prunioo  13442  fseq1p1m1  13559  fzshftral  13576  seqp1d  13983  seqf1olem2  14007  seqfeq4  14016  binom3  14189  expmulnbnd  14200  discr  14205  bcn2  14284  hashun2  14348  hashun3  14349  hashdif  14378  hashgt12el  14387  hashgt12el2  14388  hashfacen  14419  s2prop  14873  s4prop  14876  s3sndisj  14933  s3iunsndisj  14934  cnrecnv  15131  rddif  15307  amgm2  15336  rlimres  15524  lo1res  15525  iseraltlem2  15649  iseralt  15651  fsumss  15691  fsumcl2lem  15697  isumclim3  15725  fsumcnv  15739  telfsumo  15768  fsumiun  15787  arisum2  15827  geoisum1c  15846  fprodss  15914  fprodser  15915  fprodcl2lem  15916  fprodsplit  15932  fprodn0  15945  fprodcnv  15949  iprodclim3  15966  risefac1  15999  fallfac1  16000  bpolyval  16015  bpoly3  16024  bpoly4  16025  fsumcube  16026  sinhval  16122  cos01bnd  16154  ruclem6  16203  sadadd2lem2  16420  eucalgval  16552  pcid  16844  prmreclem4  16890  4sqlem15  16930  4sqlem16  16931  ramcl  17000  strfv2d  17171  setsid  17177  imasvscafn  17500  xpsff1o  17530  xpsaddlem  17536  xpsvsca  17540  xpsle  17542  mreexexlem2d  17606  mreexexlem4d  17608  sscres  17785  xpcid  18150  evlfcllem  18182  hofcl  18220  isacs5lem  18504  frmdup3lem  18793  cayleylem2  19343  f1omvdco2  19378  symggen  19400  psgnunilem1  19423  pgp0  19526  sylow3lem2  19558  lsmdisjr  19614  lsmdisj2r  19615  subgdisj2  19622  efgval  19647  frgpuplem  19702  frgpup2  19706  gsumval3  19837  gsumzres  19839  gsum2d2lem  19903  dprdf1  19965  dmdprdsplit2lem  19977  dmdprdsplit2  19978  ablfaclem3  20019  prdsmgp  20060  unitgrp  20292  subdrgint  20712  crng2idl  21191  gsumfsum  21351  pzriprnglem6  21396  chrid  21435  znleval  21464  frgpcyg  21483  ocv1  21588  frlmip  21687  ellspd  21711  psrass1lem  21841  ply1chr  22193  evl1var  22223  pf1mpf  22239  pf1ind  22242  mamuvs2  22293  madurid  22531  baspartn  22841  mretopd  22979  ordtcld1  23084  ordtcld2  23085  leordtvallem1  23097  leordtvallem2  23098  paste  23181  imacmp  23284  cmpsub  23287  unconn  23316  1stckgen  23441  ptbasfi  23468  txcld  23490  ptclsg  23502  txdis1cn  23522  ptrescn  23526  hausdiag  23532  txkgen  23539  xkoptsub  23541  xkococnlem  23546  cnmpt21  23558  cnmpt22  23561  tgqtop  23599  qtoprest  23604  kqdisj  23619  hmeores  23658  hmphindis  23684  pt1hmeo  23693  ptuncnv  23694  ptunhmeo  23695  xpstopnlem1  23696  xkohmeo  23702  alexsublem  23931  ptcmplem2  23940  tmdcn2  23976  cldsubg  23998  qustgplem  24008  tsmsres  24031  ustbas2  24113  ressuss  24150  metreslem  24250  xpsdsval  24269  prdsxmslem2  24417  txmetcnp  24435  tngngp  24542  nrmtngdist  24545  remetdval  24677  cnheibor  24854  evth2  24859  pcoass  24924  ncvspi  25056  iscmet3  25193  rrxip  25290  minveclem2  25326  cmmbl  25435  nulmbl2  25437  volinun  25447  voliunlem1  25451  volsup  25457  ovolioo  25469  uniiccdif  25479  uniioombllem2  25484  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  ismbf3d  25555  itg2uba  25644  itg2i1fseq  25656  itgsplitioo  25739  limcflf  25782  cnplimc  25788  limcun  25796  dvfval  25798  dvres  25812  dvres3a  25815  dvnp1  25827  dvn1  25828  dvexp3  25882  dvsincos  25885  mvth  25897  c1lip2  25903  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgsubstlem  25955  itgsubst  25956  coeeq2  26147  dgreq0  26171  dgrcolem2  26180  vieta1  26220  ulm2  26294  radcnv0  26325  abelthlem2  26342  tanarg  26528  advlogexp  26564  efopn  26567  logtayl  26569  cxpcn3  26658  ang180lem3  26721  quad2  26749  mcubic  26757  binom4  26760  dquart  26763  quart1lem  26765  quart1  26766  quartlem1  26767  asinlem3a  26780  efiatan  26822  tanatan  26829  atanbndlem  26835  dvatan  26845  wilthlem2  26979  ftalem3  26985  ftalem5  26987  basellem3  26993  mumullem2  27090  musum  27101  mpodvdsmulf1o  27104  chtublem  27122  perfectlem2  27141  bposlem6  27200  bposlem9  27203  1lgs  27251  lgs1  27252  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgsquadlem2  27292  lgsquad2lem2  27296  2sqblem  27342  rpvmasum2  27423  log2sumbnd  27455  noetasuplem4  27648  sltlpss  27819  slelss  27820  opphllem3  28676  vtxdun  29409  clwwlknon2num  30034  eucrct2eupth  30174  ex-fpar  30391  nvpi  30596  nvop  30605  phop  30747  minvecolem2  30804  hi01  31025  pjchi  31361  chjidm  31449  mayete3i  31657  ho0val  31679  lnop0  31895  adjbdlnb  32013  pjin2i  32122  mdslmd3i  32261  mdexchi  32264  imadifxp  32530  fcoinver  32533  suppovss  32604  fressupp  32611  supppreima  32614  mptprop  32621  padct  32643  f1od2  32644  fcobijfs  32646  ffsrn  32652  iocinif  32704  difioo  32705  indf1ofs  32789  s2rnOLD  32865  s3rnOLD  32867  cshw1s2  32882  gsummpt2co  32988  gsumhashmul  33001  symgfcoeu  33039  symgcom  33040  pmtrprfv2  33045  pmtrcnel2  33047  tocyc01  33075  cycpmconjv  33099  cycpmconjs  33113  elrgspnlem2  33194  ofldchr  33292  lsmsnorb2  33363  krull  33450  opprqusbas  33459  opprqusplusg  33460  qsdrngi  33466  rgmoddimOLD  33606  ply1degltdimlem  33618  lindsun  33621  dimkerim  33623  fldexttr  33654  constrcon  33764  cos9thpiminplylem3  33774  smatlem  33787  zarcmplem  33871  esumpad2  34046  hasheuni  34075  esumcvg2  34077  esum2dlem  34082  sigapildsys  34152  measxun2  34200  measunl  34206  measinblem  34210  carsgclctunlem1  34308  carsgclctunlem3  34311  sibfof  34331  sitgclg  34333  eulerpartlemgf  34370  probdif  34411  cndprobval  34424  ballotlemic  34498  signsvtn0  34561  signstres  34566  chtvalz  34620  hgt750lemd  34639  bnj1415  35028  f1resrcmplf1d  35077  f1resfz0f1d  35101  revwlk  35112  subfacp1lem1  35166  subfacp1lem3  35169  subfacp1lem5  35171  cvmscld  35260  cvmlift2lem9a  35290  cvmlift2lem9  35298  fwddifnp1  36153  finxpreclem5  37383  ptrest  37613  poimirlem2  37616  poimirlem3  37617  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  poimirlem25  37639  poimirlem27  37641  poimirlem28  37642  poimirlem29  37643  poimirlem31  37645  voliunnfl  37658  volsupnfl  37659  mbfresfi  37660  itg2addnclem2  37666  itg2addnclem3  37667  ftc1anclem5  37691  dvacos  37699  areacirclem5  37706  cocnv  37719  istotbnd3  37765  ssbnd  37782  disjresdisj  38229  eccnvepres3  38274  symrelim  38550  osumcllem9N  39958  4atexlemex2  40065  cdleme20j  40312  cdlemg47  40730  diaintclN  41052  dibintclN  41161  dihintcl  41338  lclkrlem2e  41505  lclkrlem2p  41516  lcfrlem31  41567  lcmineqlem  42040  sticksstones8  42141  dvun  42347  readdlid  42391  evlsvvval  42551  selvvvval  42573  fsuppssind  42581  prjspnval2  42606  flt4lem  42633  diophin  42760  monotuz  42930  monotoddzzfi  42931  oddcomabszz  42933  fnwe2val  43038  lnmlmic  43077  fiuneneq  43181  cytpval  43191  oaun3  43371  ntrkbimka  44027  ntrneifv2  44069  mnringmulrd  44212  mnringmulrcld  44217  radcnvrat  44303  nzprmdif  44308  binomcxplemnotnn0  44345  ioccncflimc  45883  icocncflimc  45887  stoweidlem50  46048  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem107  46211  lambert0  46888  lamberte  46889  elsprel  47476  reuopreuprim  47527  perfectALTVlem2  47723  dfnbgr6  47857  dfsclnbgr6  47858  restclssep  48904  seposep  48914  iscnrm3rlem8  48935  swapfid  49268  cofuswapf1  49283  cofuswapf2  49284  idfudiag1lem  49512  termcfuncval  49521  ranval  49609  lmddu  49656  initocmd  49658  logb2aval  49753  aacllem  49790