Theorem eqtr3id 2791

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 2789	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3eqtr3g  2800  csbeq1a  3913  ssdifeq0  4487  pofun  5610  opabbi2dv  5860  cnvsng  6243  csbpredg  6327  funcnvpr  6628  funcnvtp  6629  funcnvqp  6630  f1imadifssran  6652  fresin  6777  fresaunres2  6780  f1imacnv  6864  foimacnv  6865  funfv  6996  dffv2  7004  fimacnvinrn  7091  rescnvimafod  7093  fsn2  7156  funiunfvf  7269  fcof1oinvd  7313  riotaxfrd  7422  f1opw2  7688  fnexALT  7975  fparlem3  8139  fparlem4  8140  fsplitfpar  8143  fvproj  8159  mpocurryd  8294  seqomlem1  8490  seqomlem4  8493  oasuc  8562  oesuclem  8563  omsuc  8564  onasuc  8566  onmsuc  8567  eqerlem  8780  pmresg  8910  fopwdom  9120  sbthlem8  9130  sbthlem9  9131  fodomr  9168  domss2  9176  mapen  9181  cnvfi  9216  enp1iOLD  9314  xpfiOLD  9359  fiint  9366  fiintOLD  9367  fodomfir  9368  f1opwfi  9396  mapfien  9448  marypha1lem  9473  unxpwdom  9629  cantnfval2  9709  ttrcltr  9756  infxpenlem  10053  djuinf  10229  isf34lem3  10415  isf34lem5  10418  axdc4lem  10495  ttukeylem6  10554  rankcf  10817  tskuni  10823  gruima  10842  dmrecnq  11008  ltexnq  11015  reclem3pr  11089  pn0sr  11141  mulgt0sr  11145  recdiv  11973  2resupmax  13230  max0sub  13238  rexmul  13313  xmulmnf1  13318  xmulm1  13323  prunioo  13521  fseq1p1m1  13638  fzshftral  13655  seqp1d  14059  seqf1olem2  14083  seqfeq4  14092  binom3  14263  expmulnbnd  14274  discr  14279  bcn2  14358  hashun2  14422  hashun3  14423  hashdif  14452  hashgt12el  14461  hashgt12el2  14462  hashfacen  14493  s2prop  14946  s4prop  14949  s3sndisj  15006  s3iunsndisj  15007  cnrecnv  15204  rddif  15379  amgm2  15408  rlimres  15594  lo1res  15595  iseraltlem2  15719  iseralt  15721  fsumss  15761  fsumcl2lem  15767  isumclim3  15795  fsumcnv  15809  telfsumo  15838  fsumiun  15857  arisum2  15897  geoisum1c  15916  fprodss  15984  fprodser  15985  fprodcl2lem  15986  fprodsplit  16002  fprodn0  16015  fprodcnv  16019  iprodclim3  16036  risefac1  16069  fallfac1  16070  bpolyval  16085  bpoly3  16094  bpoly4  16095  fsumcube  16096  sinhval  16190  cos01bnd  16222  ruclem6  16271  sadadd2lem2  16487  eucalgval  16619  pcid  16911  prmreclem4  16957  4sqlem15  16997  4sqlem16  16998  ramcl  17067  strfv2d  17238  setsid  17244  imasvscafn  17582  xpsff1o  17612  xpsaddlem  17618  xpsvsca  17622  xpsle  17624  mreexexlem2d  17688  mreexexlem4d  17690  sscres  17867  xpcid  18234  evlfcllem  18266  hofcl  18304  isacs5lem  18590  frmdup3lem  18879  cayleylem2  19431  f1omvdco2  19466  symggen  19488  psgnunilem1  19511  pgp0  19614  sylow3lem2  19646  lsmdisjr  19702  lsmdisj2r  19703  subgdisj2  19710  efgval  19735  frgpuplem  19790  frgpup2  19794  gsumval3  19925  gsumzres  19927  gsum2d2lem  19991  dprdf1  20053  dmdprdsplit2lem  20065  dmdprdsplit2  20066  ablfaclem3  20107  prdsmgp  20148  unitgrp  20383  subdrgint  20804  crng2idl  21291  gsumfsum  21452  pzriprnglem6  21497  chrid  21540  znleval  21573  frgpcyg  21592  ocv1  21697  frlmip  21798  ellspd  21822  psrass1lem  21952  ply1chr  22310  evl1var  22340  pf1mpf  22356  pf1ind  22359  mamuvs2  22410  madurid  22650  baspartn  22961  mretopd  23100  ordtcld1  23205  ordtcld2  23206  leordtvallem1  23218  leordtvallem2  23219  paste  23302  imacmp  23405  cmpsub  23408  unconn  23437  1stckgen  23562  ptbasfi  23589  txcld  23611  ptclsg  23623  txdis1cn  23643  ptrescn  23647  hausdiag  23653  txkgen  23660  xkoptsub  23662  xkococnlem  23667  cnmpt21  23679  cnmpt22  23682  tgqtop  23720  qtoprest  23725  kqdisj  23740  hmeores  23779  hmphindis  23805  pt1hmeo  23814  ptuncnv  23815  ptunhmeo  23816  xpstopnlem1  23817  xkohmeo  23823  alexsublem  24052  ptcmplem2  24061  tmdcn2  24097  cldsubg  24119  qustgplem  24129  tsmsres  24152  ustbas2  24234  ressuss  24271  metreslem  24372  xpsdsval  24391  prdsxmslem2  24542  txmetcnp  24560  tngngp  24675  nrmtngdist  24678  remetdval  24810  cnheibor  24987  evth2  24992  pcoass  25057  ncvspi  25190  iscmet3  25327  rrxip  25424  minveclem2  25460  cmmbl  25569  nulmbl2  25571  volinun  25581  voliunlem1  25585  volsup  25591  ovolioo  25603  uniiccdif  25613  uniioombllem2  25618  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  ismbf3d  25689  itg2uba  25778  itg2i1fseq  25790  itgsplitioo  25873  limcflf  25916  cnplimc  25922  limcun  25930  dvfval  25932  dvres  25946  dvres3a  25949  dvnp1  25961  dvn1  25962  dvexp3  26016  dvsincos  26019  mvth  26031  c1lip2  26037  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubstlem  26089  itgsubst  26090  coeeq2  26281  dgreq0  26305  dgrcolem2  26314  vieta1  26354  ulm2  26428  radcnv0  26459  abelthlem2  26476  tanarg  26661  advlogexp  26697  efopn  26700  logtayl  26702  cxpcn3  26791  ang180lem3  26854  quad2  26882  mcubic  26890  binom4  26893  dquart  26896  quart1lem  26898  quart1  26899  quartlem1  26900  asinlem3a  26913  efiatan  26955  tanatan  26962  atanbndlem  26968  dvatan  26978  wilthlem2  27112  ftalem3  27118  ftalem5  27120  basellem3  27126  mumullem2  27223  musum  27234  mpodvdsmulf1o  27237  chtublem  27255  perfectlem2  27274  bposlem6  27333  bposlem9  27336  1lgs  27384  lgs1  27385  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgsquadlem2  27425  lgsquad2lem2  27429  2sqblem  27475  rpvmasum2  27556  log2sumbnd  27588  noetasuplem4  27781  sltlpss  27945  slelss  27946  opphllem3  28757  vtxdun  29499  clwwlknon2num  30124  eucrct2eupth  30264  ex-fpar  30481  nvpi  30686  nvop  30695  phop  30837  minvecolem2  30894  hi01  31115  pjchi  31451  chjidm  31539  mayete3i  31747  ho0val  31769  lnop0  31985  adjbdlnb  32103  pjin2i  32212  mdslmd3i  32351  mdexchi  32354  imadifxp  32614  fcoinver  32617  suppovss  32690  fressupp  32697  supppreima  32700  mptprop  32707  padct  32731  f1od2  32732  fcobijfs  32734  ffsrn  32740  iocinif  32783  difioo  32784  indf1ofs  32851  s2rnOLD  32928  s3rnOLD  32930  cshw1s2  32945  gsummpt2co  33051  gsumhashmul  33064  symgfcoeu  33102  symgcom  33103  pmtrprfv2  33108  pmtrcnel2  33110  tocyc01  33138  cycpmconjv  33162  cycpmconjs  33176  elrgspnlem2  33247  ofldchr  33344  lsmsnorb2  33420  krull  33507  opprqusbas  33516  opprqusplusg  33517  qsdrngi  33523  rgmoddimOLD  33661  ply1degltdimlem  33673  lindsun  33676  dimkerim  33678  fldexttr  33709  smatlem  33796  zarcmplem  33880  esumpad2  34057  hasheuni  34086  esumcvg2  34088  esum2dlem  34093  sigapildsys  34163  measxun2  34211  measunl  34217  measinblem  34221  carsgclctunlem1  34319  carsgclctunlem3  34322  sibfof  34342  sitgclg  34344  eulerpartlemgf  34381  probdif  34422  cndprobval  34435  ballotlemic  34509  signsvtn0  34585  signstres  34590  chtvalz  34644  hgt750lemd  34663  bnj1415  35052  f1resrcmplf1d  35101  f1resfz0f1d  35119  revwlk  35130  subfacp1lem1  35184  subfacp1lem3  35187  subfacp1lem5  35189  cvmscld  35278  cvmlift2lem9a  35308  cvmlift2lem9  35316  fwddifnp1  36166  finxpreclem5  37396  ptrest  37626  poimirlem2  37629  poimirlem3  37630  poimirlem6  37633  poimirlem7  37634  poimirlem9  37636  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem24  37651  poimirlem25  37652  poimirlem27  37654  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  voliunnfl  37671  volsupnfl  37672  mbfresfi  37673  itg2addnclem2  37679  itg2addnclem3  37680  ftc1anclem5  37704  dvacos  37712  areacirclem5  37719  cocnv  37732  istotbnd3  37778  ssbnd  37795  disjresdisj  38242  eccnvepres3  38287  symrelim  38560  osumcllem9N  39966  4atexlemex2  40073  cdleme20j  40320  cdlemg47  40738  diaintclN  41060  dibintclN  41169  dihintcl  41346  lclkrlem2e  41513  lclkrlem2p  41524  lcfrlem31  41575  lcmineqlem  42053  sticksstones8  42154  dvun  42389  readdlid  42433  evlsvvval  42573  selvvvval  42595  fsuppssind  42603  prjspnval2  42628  flt4lem  42655  diophin  42783  monotuz  42953  monotoddzzfi  42954  oddcomabszz  42956  fnwe2val  43061  lnmlmic  43100  fiuneneq  43204  cytpval  43214  oaun3  43395  ntrkbimka  44051  ntrneifv2  44093  mnringmulrd  44240  mnringmulrcld  44247  radcnvrat  44333  nzprmdif  44338  binomcxplemnotnn0  44375  ioccncflimc  45900  icocncflimc  45904  stoweidlem50  46065  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem107  46228  elsprel  47462  reuopreuprim  47513  perfectALTVlem2  47709  dfnbgr6  47843  dfsclnbgr6  47844  restclssep  48813  seposep  48823  iscnrm3rlem8  48844  swapfid  48985  cofuswapf1  48994  cofuswapf2  48995  logb2aval  49283  aacllem  49320