Theorem eqtr3id 2794

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  3eqtr3g  2803  csbeq1a  3935  ssdifeq0  4510  pofun  5626  opabbi2dv  5874  cnvsng  6254  csbpredg  6338  funcnvpr  6640  funcnvtp  6641  funcnvqp  6642  fresin  6790  fresaunres2  6793  f1imacnv  6878  foimacnv  6879  funfv  7009  dffv2  7017  fimacnvinrn  7105  rescnvimafod  7107  fsn2  7170  funiunfvf  7286  fcof1oinvd  7329  riotaxfrd  7439  f1opw2  7705  fnexALT  7991  fparlem3  8155  fparlem4  8156  fsplitfpar  8159  fvproj  8175  mpocurryd  8310  seqomlem1  8506  seqomlem4  8509  oasuc  8580  oesuclem  8581  omsuc  8582  onasuc  8584  onmsuc  8585  eqerlem  8798  pmresg  8928  fopwdom  9146  sbthlem8  9156  sbthlem9  9157  fodomr  9194  domss2  9202  mapen  9207  cnvfi  9243  enp1iOLD  9342  xpfiOLD  9387  fiint  9394  fiintOLD  9395  fodomfir  9396  f1opwfi  9426  mapfien  9477  marypha1lem  9502  unxpwdom  9658  cantnfval2  9738  ttrcltr  9785  infxpenlem  10082  djuinf  10258  isf34lem3  10444  isf34lem5  10447  axdc4lem  10524  ttukeylem6  10583  rankcf  10846  tskuni  10852  gruima  10871  dmrecnq  11037  ltexnq  11044  reclem3pr  11118  pn0sr  11170  mulgt0sr  11174  recdiv  12000  2resupmax  13250  max0sub  13258  rexmul  13333  xmulmnf1  13338  xmulm1  13343  prunioo  13541  fseq1p1m1  13658  fzshftral  13672  seqp1d  14069  seqf1olem2  14093  seqfeq4  14102  binom3  14273  expmulnbnd  14284  discr  14289  bcn2  14368  hashun2  14432  hashun3  14433  hashdif  14462  hashgt12el  14471  hashgt12el2  14472  hashfacen  14503  s2prop  14956  s4prop  14959  s3sndisj  15016  s3iunsndisj  15017  cnrecnv  15214  rddif  15389  amgm2  15418  rlimres  15604  lo1res  15605  iseraltlem2  15731  iseralt  15733  fsumss  15773  fsumcl2lem  15779  isumclim3  15807  fsumcnv  15821  telfsumo  15850  fsumiun  15869  arisum2  15909  geoisum1c  15928  fprodss  15996  fprodser  15997  fprodcl2lem  15998  fprodsplit  16014  fprodn0  16027  fprodcnv  16031  iprodclim3  16048  risefac1  16081  fallfac1  16082  bpolyval  16097  bpoly3  16106  bpoly4  16107  fsumcube  16108  sinhval  16202  cos01bnd  16234  ruclem6  16283  sadadd2lem2  16496  eucalgval  16629  pcid  16920  prmreclem4  16966  4sqlem15  17006  4sqlem16  17007  ramcl  17076  strfv2d  17249  setsid  17255  imasvscafn  17597  xpsff1o  17627  xpsaddlem  17633  xpsvsca  17637  xpsle  17639  mreexexlem2d  17703  mreexexlem4d  17705  sscres  17884  xpcid  18258  evlfcllem  18291  hofcl  18329  isacs5lem  18615  frmdup3lem  18901  cayleylem2  19455  f1omvdco2  19490  symggen  19512  psgnunilem1  19535  pgp0  19638  sylow3lem2  19670  lsmdisjr  19726  lsmdisj2r  19727  subgdisj2  19734  efgval  19759  frgpuplem  19814  frgpup2  19818  gsumval3  19949  gsumzres  19951  gsum2d2lem  20015  dprdf1  20077  dmdprdsplit2lem  20089  dmdprdsplit2  20090  ablfaclem3  20131  prdsmgp  20178  unitgrp  20409  subdrgint  20826  crng2idl  21314  gsumfsum  21475  pzriprnglem6  21520  chrid  21563  znleval  21596  frgpcyg  21615  ocv1  21720  frlmip  21821  ellspd  21845  psrass1lem  21975  ply1chr  22331  evl1var  22361  pf1mpf  22377  pf1ind  22380  mamuvs2  22431  madurid  22671  baspartn  22982  mretopd  23121  ordtcld1  23226  ordtcld2  23227  leordtvallem1  23239  leordtvallem2  23240  paste  23323  imacmp  23426  cmpsub  23429  unconn  23458  1stckgen  23583  ptbasfi  23610  txcld  23632  ptclsg  23644  txdis1cn  23664  ptrescn  23668  hausdiag  23674  txkgen  23681  xkoptsub  23683  xkococnlem  23688  cnmpt21  23700  cnmpt22  23703  tgqtop  23741  qtoprest  23746  kqdisj  23761  hmeores  23800  hmphindis  23826  pt1hmeo  23835  ptuncnv  23836  ptunhmeo  23837  xpstopnlem1  23838  xkohmeo  23844  alexsublem  24073  ptcmplem2  24082  tmdcn2  24118  cldsubg  24140  qustgplem  24150  tsmsres  24173  ustbas2  24255  ressuss  24292  metreslem  24393  xpsdsval  24412  prdsxmslem2  24563  txmetcnp  24581  tngngp  24696  nrmtngdist  24699  remetdval  24830  cnheibor  25006  evth2  25011  pcoass  25076  ncvspi  25209  iscmet3  25346  rrxip  25443  minveclem2  25479  cmmbl  25588  nulmbl2  25590  volinun  25600  voliunlem1  25604  volsup  25610  ovolioo  25622  uniiccdif  25632  uniioombllem2  25637  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  ismbf3d  25708  itg2uba  25798  itg2i1fseq  25810  itgsplitioo  25893  limcflf  25936  cnplimc  25942  limcun  25950  dvfval  25952  dvres  25966  dvres3a  25969  dvnp1  25981  dvn1  25982  dvexp3  26036  dvsincos  26039  mvth  26051  c1lip2  26057  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgsubstlem  26109  itgsubst  26110  coeeq2  26301  dgreq0  26325  dgrcolem2  26334  vieta1  26372  ulm2  26446  radcnv0  26477  abelthlem2  26494  tanarg  26679  advlogexp  26715  efopn  26718  logtayl  26720  cxpcn3  26809  ang180lem3  26872  quad2  26900  mcubic  26908  binom4  26911  dquart  26914  quart1lem  26916  quart1  26917  quartlem1  26918  asinlem3a  26931  efiatan  26973  tanatan  26980  atanbndlem  26986  dvatan  26996  wilthlem2  27130  ftalem3  27136  ftalem5  27138  basellem3  27144  mumullem2  27241  musum  27252  mpodvdsmulf1o  27255  chtublem  27273  perfectlem2  27292  bposlem6  27351  bposlem9  27354  1lgs  27402  lgs1  27403  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgsquadlem2  27443  lgsquad2lem2  27447  2sqblem  27493  rpvmasum2  27574  log2sumbnd  27606  noetasuplem4  27799  sltlpss  27963  slelss  27964  opphllem3  28775  vtxdun  29517  clwwlknon2num  30137  eucrct2eupth  30277  ex-fpar  30494  nvpi  30699  nvop  30708  phop  30850  minvecolem2  30907  hi01  31128  pjchi  31464  chjidm  31552  mayete3i  31760  ho0val  31782  lnop0  31998  adjbdlnb  32116  pjin2i  32225  mdslmd3i  32364  mdexchi  32367  imadifxp  32623  fcoinver  32626  suppovss  32697  fressupp  32700  supppreima  32703  mptprop  32710  padct  32733  f1od2  32735  fcobijfs  32737  ffsrn  32743  iocinif  32786  difioo  32787  s2rnOLD  32910  s3rnOLD  32912  cshw1s2  32927  gsummpt2co  33031  gsumhashmul  33040  symgfcoeu  33075  symgcom  33076  pmtrprfv2  33081  pmtrcnel2  33083  tocyc01  33111  cycpmconjv  33135  cycpmconjs  33149  ofldchr  33309  lsmsnorb2  33385  krull  33472  opprqusbas  33481  opprqusplusg  33482  qsdrngi  33488  rgmoddimOLD  33623  ply1degltdimlem  33635  lindsun  33638  dimkerim  33640  fldexttr  33671  smatlem  33743  zarcmplem  33827  indf1ofs  33990  esumpad2  34020  hasheuni  34049  esumcvg2  34051  esum2dlem  34056  sigapildsys  34126  measxun2  34174  measunl  34180  measinblem  34184  carsgclctunlem1  34282  carsgclctunlem3  34285  sibfof  34305  sitgclg  34307  eulerpartlemgf  34344  probdif  34385  cndprobval  34398  ballotlemic  34471  signsvtn0  34547  signstres  34552  chtvalz  34606  hgt750lemd  34625  bnj1415  35014  f1resrcmplf1d  35063  f1resfz0f1d  35081  revwlk  35092  subfacp1lem1  35147  subfacp1lem3  35150  subfacp1lem5  35152  cvmscld  35241  cvmlift2lem9a  35271  cvmlift2lem9  35279  fwddifnp1  36129  finxpreclem5  37361  ptrest  37579  poimirlem2  37582  poimirlem3  37583  poimirlem6  37586  poimirlem7  37587  poimirlem9  37589  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  poimirlem25  37605  poimirlem27  37607  poimirlem28  37608  poimirlem29  37609  poimirlem31  37611  voliunnfl  37624  volsupnfl  37625  mbfresfi  37626  itg2addnclem2  37632  itg2addnclem3  37633  ftc1anclem5  37657  dvacos  37665  areacirclem5  37672  cocnv  37685  istotbnd3  37731  ssbnd  37748  disjresdisj  38196  eccnvepres3  38242  symrelim  38515  osumcllem9N  39921  4atexlemex2  40028  cdleme20j  40275  cdlemg47  40693  diaintclN  41015  dibintclN  41124  dihintcl  41301  lclkrlem2e  41468  lclkrlem2p  41479  lcfrlem31  41530  lcmineqlem  42009  sticksstones8  42110  readdlid  42379  evlsvvval  42518  selvvvval  42540  fsuppssind  42548  prjspnval2  42573  flt4lem  42600  diophin  42728  monotuz  42898  monotoddzzfi  42899  oddcomabszz  42901  fnwe2val  43006  lnmlmic  43045  fiuneneq  43153  cytpval  43163  oaun3  43344  ntrkbimka  44000  ntrneifv2  44042  mnringmulrd  44190  mnringmulrcld  44197  radcnvrat  44283  nzprmdif  44288  binomcxplemnotnn0  44325  ioccncflimc  45806  icocncflimc  45810  stoweidlem50  45971  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem107  46134  elsprel  47349  reuopreuprim  47400  perfectALTVlem2  47596  dfnbgr6  47729  dfsclnbgr6  47730  restclssep  48595  seposep  48605  iscnrm3rlem8  48627  logb2aval  48856  aacllem  48895