Theorem eqtr3id 2780

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  3eqtr3g  2789  csbeq1a  3859  ssdifeq0  4432  pofun  5537  opabbi2dv  5784  cnvsng  6165  csbpredg  6249  funcnvpr  6538  funcnvtp  6539  funcnvqp  6540  f1imadifssran  6562  fresin  6687  fresaunres2  6690  f1imacnv  6774  foimacnv  6775  funfv  6904  dffv2  6912  fimacnvinrn  6999  rescnvimafod  7001  fsn2  7064  funiunfvf  7178  fcof1oinvd  7222  riotaxfrd  7332  f1opw2  7596  fnexALT  7878  fparlem3  8039  fparlem4  8040  fsplitfpar  8043  fvproj  8059  mpocurryd  8194  seqomlem1  8364  seqomlem4  8367  oasuc  8434  oesuclem  8435  omsuc  8436  onasuc  8438  onmsuc  8439  eqerlem  8652  pmresg  8789  fopwdom  8993  sbthlem8  9002  sbthlem9  9003  fodomr  9036  domss2  9044  mapen  9049  cnvfi  9080  fiint  9206  fodomfir  9207  f1opwfi  9235  mapfien  9287  marypha1lem  9312  unxpwdom  9470  cantnfval2  9554  ttrcltr  9601  infxpenlem  9899  djuinf  10075  isf34lem3  10261  isf34lem5  10264  axdc4lem  10341  ttukeylem6  10400  rankcf  10663  tskuni  10669  gruima  10688  dmrecnq  10854  ltexnq  10861  reclem3pr  10935  pn0sr  10987  mulgt0sr  10991  recdiv  11822  2resupmax  13082  max0sub  13090  rexmul  13165  xmulmnf1  13170  xmulm1  13175  prunioo  13376  fseq1p1m1  13493  fzshftral  13510  seqp1d  13920  seqf1olem2  13944  seqfeq4  13953  binom3  14126  expmulnbnd  14137  discr  14142  bcn2  14221  hashun2  14285  hashun3  14286  hashdif  14315  hashgt12el  14324  hashgt12el2  14325  hashfacen  14356  s2prop  14809  s4prop  14812  s3sndisj  14869  s3iunsndisj  14870  cnrecnv  15067  rddif  15243  amgm2  15272  rlimres  15460  lo1res  15461  iseraltlem2  15585  iseralt  15587  fsumss  15627  fsumcl2lem  15633  isumclim3  15661  fsumcnv  15675  telfsumo  15704  fsumiun  15723  arisum2  15763  geoisum1c  15782  fprodss  15850  fprodser  15851  fprodcl2lem  15852  fprodsplit  15868  fprodn0  15881  fprodcnv  15885  iprodclim3  15902  risefac1  15935  fallfac1  15936  bpolyval  15951  bpoly3  15960  bpoly4  15961  fsumcube  15962  sinhval  16058  cos01bnd  16090  ruclem6  16139  sadadd2lem2  16356  eucalgval  16488  pcid  16780  prmreclem4  16826  4sqlem15  16866  4sqlem16  16867  ramcl  16936  strfv2d  17107  setsid  17113  imasvscafn  17436  xpsff1o  17466  xpsaddlem  17472  xpsvsca  17476  xpsle  17478  mreexexlem2d  17546  mreexexlem4d  17548  sscres  17725  xpcid  18090  evlfcllem  18122  hofcl  18160  isacs5lem  18446  frmdup3lem  18769  cayleylem2  19320  f1omvdco2  19355  symggen  19377  psgnunilem1  19400  pgp0  19503  sylow3lem2  19535  lsmdisjr  19591  lsmdisj2r  19592  subgdisj2  19599  efgval  19624  frgpuplem  19679  frgpup2  19683  gsumval3  19814  gsumzres  19816  gsum2d2lem  19880  dprdf1  19942  dmdprdsplit2lem  19954  dmdprdsplit2  19955  ablfaclem3  19996  prdsmgp  20064  unitgrp  20296  subdrgint  20713  crng2idl  21213  gsumfsum  21366  pzriprnglem6  21418  chrid  21457  znleval  21486  frgpcyg  21505  ofldchr  21508  ocv1  21611  frlmip  21710  ellspd  21734  psrass1lem  21864  ply1chr  22216  evl1var  22246  pf1mpf  22262  pf1ind  22265  mamuvs2  22316  madurid  22554  baspartn  22864  mretopd  23002  ordtcld1  23107  ordtcld2  23108  leordtvallem1  23120  leordtvallem2  23121  paste  23204  imacmp  23307  cmpsub  23310  unconn  23339  1stckgen  23464  ptbasfi  23491  txcld  23513  ptclsg  23525  txdis1cn  23545  ptrescn  23549  hausdiag  23555  txkgen  23562  xkoptsub  23564  xkococnlem  23569  cnmpt21  23581  cnmpt22  23584  tgqtop  23622  qtoprest  23627  kqdisj  23642  hmeores  23681  hmphindis  23707  pt1hmeo  23716  ptuncnv  23717  ptunhmeo  23718  xpstopnlem1  23719  xkohmeo  23725  alexsublem  23954  ptcmplem2  23963  tmdcn2  23999  cldsubg  24021  qustgplem  24031  tsmsres  24054  ustbas2  24135  ressuss  24172  metreslem  24272  xpsdsval  24291  prdsxmslem2  24439  txmetcnp  24457  tngngp  24564  nrmtngdist  24567  remetdval  24699  cnheibor  24876  evth2  24881  pcoass  24946  ncvspi  25078  iscmet3  25215  rrxip  25312  minveclem2  25348  cmmbl  25457  nulmbl2  25459  volinun  25469  voliunlem1  25473  volsup  25479  ovolioo  25491  uniiccdif  25501  uniioombllem2  25506  uniioombllem3  25508  uniioombllem4  25509  uniioombllem5  25510  ismbf3d  25577  itg2uba  25666  itg2i1fseq  25678  itgsplitioo  25761  limcflf  25804  cnplimc  25810  limcun  25818  dvfval  25820  dvres  25834  dvres3a  25837  dvnp1  25849  dvn1  25850  dvexp3  25904  dvsincos  25907  mvth  25919  c1lip2  25925  dvfsumlem2  25955  dvfsumlem2OLD  25956  itgsubstlem  25977  itgsubst  25978  coeeq2  26169  dgreq0  26193  dgrcolem2  26202  vieta1  26242  ulm2  26316  radcnv0  26347  abelthlem2  26364  tanarg  26550  advlogexp  26586  efopn  26589  logtayl  26591  cxpcn3  26680  ang180lem3  26743  quad2  26771  mcubic  26779  binom4  26782  dquart  26785  quart1lem  26787  quart1  26788  quartlem1  26789  asinlem3a  26802  efiatan  26844  tanatan  26851  atanbndlem  26857  dvatan  26867  wilthlem2  27001  ftalem3  27007  ftalem5  27009  basellem3  27015  mumullem2  27112  musum  27123  mpodvdsmulf1o  27126  chtublem  27144  perfectlem2  27163  bposlem6  27222  bposlem9  27225  1lgs  27273  lgs1  27274  lgseisenlem1  27308  lgseisenlem2  27309  lgseisenlem3  27310  lgsquadlem2  27314  lgsquad2lem2  27318  2sqblem  27364  rpvmasum2  27445  log2sumbnd  27477  noetasuplem4  27670  sltlpss  27848  slelss  27849  zs12half  28385  opphllem3  28722  vtxdun  29455  clwwlknon2num  30077  eucrct2eupth  30217  ex-fpar  30434  nvpi  30639  nvop  30648  phop  30790  minvecolem2  30847  hi01  31068  pjchi  31404  chjidm  31492  mayete3i  31700  ho0val  31722  lnop0  31938  adjbdlnb  32056  pjin2i  32165  mdslmd3i  32304  mdexchi  32307  imadifxp  32573  fcoinver  32576  suppovss  32654  fressupp  32661  supppreima  32664  mptprop  32671  padct  32693  f1od2  32694  fcobijfs  32696  ffsrn  32703  iocinif  32756  difioo  32757  indf1ofs  32839  s2rnOLD  32917  s3rnOLD  32919  cshw1s2  32933  gsummpt2co  33020  gsumhashmul  33033  symgfcoeu  33043  symgcom  33044  pmtrprfv2  33049  pmtrcnel2  33051  tocyc01  33079  cycpmconjv  33103  cycpmconjs  33117  elrgspnlem2  33202  lsmsnorb2  33349  krull  33436  opprqusbas  33445  opprqusplusg  33446  qsdrngi  33452  rgmoddimOLD  33615  ply1degltdimlem  33627  lindsun  33630  dimkerim  33632  fldexttr  33663  constrcon  33779  cos9thpiminplylem3  33789  smatlem  33802  zarcmplem  33886  esumpad2  34061  hasheuni  34090  esumcvg2  34092  esum2dlem  34097  sigapildsys  34167  measxun2  34215  measunl  34221  measinblem  34225  carsgclctunlem1  34322  carsgclctunlem3  34325  sibfof  34345  sitgclg  34347  eulerpartlemgf  34384  probdif  34425  cndprobval  34438  ballotlemic  34512  signsvtn0  34575  signstres  34580  chtvalz  34634  hgt750lemd  34653  bnj1415  35042  f1resrcmplf1d  35091  f1resfz0f1d  35150  revwlk  35161  subfacp1lem1  35215  subfacp1lem3  35218  subfacp1lem5  35220  cvmscld  35309  cvmlift2lem9a  35339  cvmlift2lem9  35347  fwddifnp1  36199  finxpreclem5  37429  ptrest  37659  poimirlem2  37662  poimirlem3  37663  poimirlem6  37666  poimirlem7  37667  poimirlem9  37669  poimirlem11  37671  poimirlem12  37672  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem24  37684  poimirlem25  37685  poimirlem27  37687  poimirlem28  37688  poimirlem29  37689  poimirlem31  37691  voliunnfl  37704  volsupnfl  37705  mbfresfi  37706  itg2addnclem2  37712  itg2addnclem3  37713  ftc1anclem5  37737  dvacos  37745  areacirclem5  37752  cocnv  37765  istotbnd3  37811  ssbnd  37828  disjresdisj  38275  eccnvepres3  38320  symrelim  38596  osumcllem9N  40003  4atexlemex2  40110  cdleme20j  40357  cdlemg47  40775  diaintclN  41097  dibintclN  41206  dihintcl  41383  lclkrlem2e  41550  lclkrlem2p  41561  lcfrlem31  41612  lcmineqlem  42085  sticksstones8  42186  dvun  42392  readdlid  42436  evlsvvval  42596  selvvvval  42618  fsuppssind  42626  prjspnval2  42651  flt4lem  42678  diophin  42805  monotuz  42974  monotoddzzfi  42975  oddcomabszz  42977  fnwe2val  43082  lnmlmic  43121  fiuneneq  43225  cytpval  43235  oaun3  43415  ntrkbimka  44071  ntrneifv2  44113  mnringmulrd  44256  mnringmulrcld  44261  radcnvrat  44347  nzprmdif  44352  binomcxplemnotnn0  44389  ioccncflimc  45923  icocncflimc  45927  stoweidlem50  46088  fourierdlem89  46233  fourierdlem90  46234  fourierdlem91  46235  fourierdlem107  46251  lambert0  46918  lamberte  46919  elsprel  47506  reuopreuprim  47557  perfectALTVlem2  47753  dfnbgr6  47888  dfsclnbgr6  47889  restclssep  48947  seposep  48957  iscnrm3rlem8  48978  swapfid  49311  cofuswapf1  49326  cofuswapf2  49327  idfudiag1lem  49555  termcfuncval  49564  ranval  49652  lmddu  49699  initocmd  49701  logb2aval  49796  aacllem  49833