Theorem eqtr3id 2784

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

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

This theorem is referenced by:  3eqtr3g  2793  csbeq1a  3888  ssdifeq0  4462  pofun  5579  opabbi2dv  5829  cnvsng  6212  csbpredg  6296  funcnvpr  6597  funcnvtp  6598  funcnvqp  6599  f1imadifssran  6621  fresin  6746  fresaunres2  6749  f1imacnv  6833  foimacnv  6834  funfv  6965  dffv2  6973  fimacnvinrn  7060  rescnvimafod  7062  fsn2  7125  funiunfvf  7240  fcof1oinvd  7285  riotaxfrd  7394  f1opw2  7660  fnexALT  7947  fparlem3  8111  fparlem4  8112  fsplitfpar  8115  fvproj  8131  mpocurryd  8266  seqomlem1  8462  seqomlem4  8465  oasuc  8534  oesuclem  8535  omsuc  8536  onasuc  8538  onmsuc  8539  eqerlem  8752  pmresg  8882  fopwdom  9092  sbthlem8  9102  sbthlem9  9103  fodomr  9140  domss2  9148  mapen  9153  cnvfi  9188  enp1iOLD  9284  xpfiOLD  9329  fiint  9336  fiintOLD  9337  fodomfir  9338  f1opwfi  9366  mapfien  9418  marypha1lem  9443  unxpwdom  9601  cantnfval2  9681  ttrcltr  9728  infxpenlem  10025  djuinf  10201  isf34lem3  10387  isf34lem5  10390  axdc4lem  10467  ttukeylem6  10526  rankcf  10789  tskuni  10795  gruima  10814  dmrecnq  10980  ltexnq  10987  reclem3pr  11061  pn0sr  11113  mulgt0sr  11117  recdiv  11945  2resupmax  13202  max0sub  13210  rexmul  13285  xmulmnf1  13290  xmulm1  13295  prunioo  13496  fseq1p1m1  13613  fzshftral  13630  seqp1d  14034  seqf1olem2  14058  seqfeq4  14067  binom3  14240  expmulnbnd  14251  discr  14256  bcn2  14335  hashun2  14399  hashun3  14400  hashdif  14429  hashgt12el  14438  hashgt12el2  14439  hashfacen  14470  s2prop  14924  s4prop  14927  s3sndisj  14984  s3iunsndisj  14985  cnrecnv  15182  rddif  15357  amgm2  15386  rlimres  15572  lo1res  15573  iseraltlem2  15697  iseralt  15699  fsumss  15739  fsumcl2lem  15745  isumclim3  15773  fsumcnv  15787  telfsumo  15816  fsumiun  15835  arisum2  15875  geoisum1c  15894  fprodss  15962  fprodser  15963  fprodcl2lem  15964  fprodsplit  15980  fprodn0  15993  fprodcnv  15997  iprodclim3  16014  risefac1  16047  fallfac1  16048  bpolyval  16063  bpoly3  16072  bpoly4  16073  fsumcube  16074  sinhval  16170  cos01bnd  16202  ruclem6  16251  sadadd2lem2  16467  eucalgval  16599  pcid  16891  prmreclem4  16937  4sqlem15  16977  4sqlem16  16978  ramcl  17047  strfv2d  17218  setsid  17224  imasvscafn  17549  xpsff1o  17579  xpsaddlem  17585  xpsvsca  17589  xpsle  17591  mreexexlem2d  17655  mreexexlem4d  17657  sscres  17834  xpcid  18199  evlfcllem  18231  hofcl  18269  isacs5lem  18553  frmdup3lem  18842  cayleylem2  19392  f1omvdco2  19427  symggen  19449  psgnunilem1  19472  pgp0  19575  sylow3lem2  19607  lsmdisjr  19663  lsmdisj2r  19664  subgdisj2  19671  efgval  19696  frgpuplem  19751  frgpup2  19755  gsumval3  19886  gsumzres  19888  gsum2d2lem  19952  dprdf1  20014  dmdprdsplit2lem  20026  dmdprdsplit2  20027  ablfaclem3  20068  prdsmgp  20109  unitgrp  20341  subdrgint  20761  crng2idl  21240  gsumfsum  21400  pzriprnglem6  21445  chrid  21484  znleval  21513  frgpcyg  21532  ocv1  21637  frlmip  21736  ellspd  21760  psrass1lem  21890  ply1chr  22242  evl1var  22272  pf1mpf  22288  pf1ind  22291  mamuvs2  22342  madurid  22580  baspartn  22890  mretopd  23028  ordtcld1  23133  ordtcld2  23134  leordtvallem1  23146  leordtvallem2  23147  paste  23230  imacmp  23333  cmpsub  23336  unconn  23365  1stckgen  23490  ptbasfi  23517  txcld  23539  ptclsg  23551  txdis1cn  23571  ptrescn  23575  hausdiag  23581  txkgen  23588  xkoptsub  23590  xkococnlem  23595  cnmpt21  23607  cnmpt22  23610  tgqtop  23648  qtoprest  23653  kqdisj  23668  hmeores  23707  hmphindis  23733  pt1hmeo  23742  ptuncnv  23743  ptunhmeo  23744  xpstopnlem1  23745  xkohmeo  23751  alexsublem  23980  ptcmplem2  23989  tmdcn2  24025  cldsubg  24047  qustgplem  24057  tsmsres  24080  ustbas2  24162  ressuss  24199  metreslem  24299  xpsdsval  24318  prdsxmslem2  24466  txmetcnp  24484  tngngp  24591  nrmtngdist  24594  remetdval  24726  cnheibor  24903  evth2  24908  pcoass  24973  ncvspi  25106  iscmet3  25243  rrxip  25340  minveclem2  25376  cmmbl  25485  nulmbl2  25487  volinun  25497  voliunlem1  25501  volsup  25507  ovolioo  25519  uniiccdif  25529  uniioombllem2  25534  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  ismbf3d  25605  itg2uba  25694  itg2i1fseq  25706  itgsplitioo  25789  limcflf  25832  cnplimc  25838  limcun  25846  dvfval  25848  dvres  25862  dvres3a  25865  dvnp1  25877  dvn1  25878  dvexp3  25932  dvsincos  25935  mvth  25947  c1lip2  25953  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgsubstlem  26005  itgsubst  26006  coeeq2  26197  dgreq0  26221  dgrcolem2  26230  vieta1  26270  ulm2  26344  radcnv0  26375  abelthlem2  26392  tanarg  26578  advlogexp  26614  efopn  26617  logtayl  26619  cxpcn3  26708  ang180lem3  26771  quad2  26799  mcubic  26807  binom4  26810  dquart  26813  quart1lem  26815  quart1  26816  quartlem1  26817  asinlem3a  26830  efiatan  26872  tanatan  26879  atanbndlem  26885  dvatan  26895  wilthlem2  27029  ftalem3  27035  ftalem5  27037  basellem3  27043  mumullem2  27140  musum  27151  mpodvdsmulf1o  27154  chtublem  27172  perfectlem2  27191  bposlem6  27250  bposlem9  27253  1lgs  27301  lgs1  27302  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgsquadlem2  27342  lgsquad2lem2  27346  2sqblem  27392  rpvmasum2  27473  log2sumbnd  27505  noetasuplem4  27698  sltlpss  27862  slelss  27863  opphllem3  28674  vtxdun  29407  clwwlknon2num  30032  eucrct2eupth  30172  ex-fpar  30389  nvpi  30594  nvop  30603  phop  30745  minvecolem2  30802  hi01  31023  pjchi  31359  chjidm  31447  mayete3i  31655  ho0val  31677  lnop0  31893  adjbdlnb  32011  pjin2i  32120  mdslmd3i  32259  mdexchi  32262  imadifxp  32528  fcoinver  32531  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  33184  ofldchr  33282  lsmsnorb2  33353  krull  33440  opprqusbas  33449  opprqusplusg  33450  qsdrngi  33456  rgmoddimOLD  33596  ply1degltdimlem  33608  lindsun  33611  dimkerim  33613  fldexttr  33646  constrcon  33754  cos9thpiminplylem3  33764  smatlem  33774  zarcmplem  33858  esumpad2  34033  hasheuni  34062  esumcvg2  34064  esum2dlem  34069  sigapildsys  34139  measxun2  34187  measunl  34193  measinblem  34197  carsgclctunlem1  34295  carsgclctunlem3  34298  sibfof  34318  sitgclg  34320  eulerpartlemgf  34357  probdif  34398  cndprobval  34411  ballotlemic  34485  signsvtn0  34548  signstres  34553  chtvalz  34607  hgt750lemd  34626  bnj1415  35015  f1resrcmplf1d  35064  f1resfz0f1d  35082  revwlk  35093  subfacp1lem1  35147  subfacp1lem3  35150  subfacp1lem5  35152  cvmscld  35241  cvmlift2lem9a  35271  cvmlift2lem9  35279  fwddifnp1  36129  finxpreclem5  37359  ptrest  37589  poimirlem2  37592  poimirlem3  37593  poimirlem6  37596  poimirlem7  37597  poimirlem9  37599  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem24  37614  poimirlem25  37615  poimirlem27  37617  poimirlem28  37618  poimirlem29  37619  poimirlem31  37621  voliunnfl  37634  volsupnfl  37635  mbfresfi  37636  itg2addnclem2  37642  itg2addnclem3  37643  ftc1anclem5  37667  dvacos  37675  areacirclem5  37682  cocnv  37695  istotbnd3  37741  ssbnd  37758  disjresdisj  38205  eccnvepres3  38250  symrelim  38523  osumcllem9N  39929  4atexlemex2  40036  cdleme20j  40283  cdlemg47  40701  diaintclN  41023  dibintclN  41132  dihintcl  41309  lclkrlem2e  41476  lclkrlem2p  41487  lcfrlem31  41538  lcmineqlem  42011  sticksstones8  42112  dvun  42349  readdlid  42393  evlsvvval  42533  selvvvval  42555  fsuppssind  42563  prjspnval2  42588  flt4lem  42615  diophin  42742  monotuz  42912  monotoddzzfi  42913  oddcomabszz  42915  fnwe2val  43020  lnmlmic  43059  fiuneneq  43163  cytpval  43173  oaun3  43353  ntrkbimka  44009  ntrneifv2  44051  mnringmulrd  44195  mnringmulrcld  44200  radcnvrat  44286  nzprmdif  44291  binomcxplemnotnn0  44328  ioccncflimc  45862  icocncflimc  45866  stoweidlem50  46027  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem107  46190  lambert0  46867  lamberte  46868  elsprel  47437  reuopreuprim  47488  perfectALTVlem2  47684  dfnbgr6  47818  dfsclnbgr6  47819  restclssep  48838  seposep  48848  iscnrm3rlem8  48869  swapfid  49144  cofuswapf1  49153  cofuswapf2  49154  idfudiag1lem  49356  termcfuncval  49365  ranval  49443  logb2aval  49576  aacllem  49613