Theorem sylan9eq 2664

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
sylan9eq.1	⊢ (𝜑 → 𝐴 = 𝐵)
sylan9eq.2	⊢ (𝜓 → 𝐵 = 𝐶)

Assertion

Ref	Expression
sylan9eq	⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sylan9eq.2	. 2 ⊢ (𝜓 → 𝐵 = 𝐶)
3		eqtr 2629	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 493	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603

This theorem is referenced by:  sylan9req  2665  sylan9eqr  2666  difeq12  3685  uneq12  3724  ineq12  3771  ifeq12  4053  ifbi  4057  ifeq12da  4068  preq12  4214  prprc  4245  opeq12  4342  opthwiener  4901  xpeq12  5058  sosn  5111  nfimad  5394  coi2  5569  funprg  5854  funtpg  5856  funcnvtp  5865  funcnvqp  5866  funcnvqpOLD  5867  funimass1  5885  f1orescnv  6065  resdif  6070  fvmpt2  6200  fvmptnf  6210  fveqressseq  6263  oveq12  6558  cbvmpt2v  6633  ovmpt2g  6693  caofinvl  6822  eqopi  7093  el2mpt2csbcl  7137  fmpt2co  7147  mpt2sn  7155  supp0cosupp0  7221  mpt2curryd  7282  fvmpt2curryd  7284  wrecseq123  7295  rdgsucmptf  7411  frsucmpt  7420  oevn0  7482  oa0r  7505  om1r  7510  oe1m  7512  omass  7547  oeoalem  7563  oeoa  7564  oeoe  7566  map0g  7783  xpcomco  7935  sbthlem4  7958  sbthlem5  7959  xpmapenlem  8012  phplem3  8026  phplem4  8027  unxpdomlem3  8051  funsnfsupp  8182  ordtypelem7  8312  cardennn  8692  dfac9  8841  cdaassen  8887  alephsing  8981  axcc3  9143  ac6num  9184  konigthlem  9269  canthp1lem2  9354  ordpipq  9643  ltrnq  9680  addclprlem2  9718  mulclprlem  9720  prlem934  9734  prlem936  9748  mulcmpblnrlem  9770  addcnsr  9835  mulcnsr  9836  axcnre  9864  recex  10538  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  xaddpnf1  11931  xaddpnf2  11932  xaddmnf1  11933  xaddmnf2  11934  rexadd  11937  xnn0xaddcl  11940  xaddnemnf  11941  xaddnepnf  11942  xadddilem  11996  addmodlteq  12607  om2uzrani  12613  om2uzrdg  12617  seqf1olem2  12703  seqf1o  12704  modexp  12861  faclbnd4lem3  12944  hashunsng  13042  lsw1  13207  swrdfv  13276  swrdccat  13344  ccats1swrdeqbi  13349  revfv  13363  cshwsublen  13393  wrdlen2  13536  wrdl2exs2  13538  wwlktovf1  13548  relexp0  13611  relexpcnv  13623  shftcan1  13671  remul2  13718  immul2  13725  sumss  14302  geomulcvg  14446  fprodss  14517  binomfallfaclem2  14610  bpolylem  14618  ef0lem  14648  efieq1re  14768  rpnnen2lem1  14782  ruclem3  14801  dvdsnegb  14837  dvdscmul  14846  dvds2ln  14852  dvds2add  14853  dvds2sub  14854  gcdn0val  15058  rpmulgcd  15113  lcmn0val  15146  odzval  15334  pcval  15387  pcmpt  15434  prmreclem4  15461  1arithlem2  15466  vdwlem8  15530  ramcl2lem  15551  ramtcl  15552  ramtub  15554  ramcl2  15558  ramcl  15571  setsval  15720  prfcl  16666  curf1cl  16691  curfcl  16695  hofcl  16722  yonedalem4c  16740  psssdm  17039  grplactval  17340  cntzval  17577  f1omvdco2  17691  pmtrfinv  17704  psgnunilem5  17737  odlem2  17781  gexlem2  17820  lsmvalx  17877  efgtval  17959  efgredlema  17976  vrgpval  18003  cyggex  18122  gsumcom2  18197  dvdsrtr  18475  abvtrivd  18663  lmhmco  18864  reslmhm  18873  lvecinv  18934  mplmon2  19314  subrgasclcl  19320  coe1fv  19397  coe1fzgsumdlem  19492  evl1gsumdlem  19541  zrhmulg  19677  znzrhval  19714  ocvval  19830  mat1dimscm  20100  dmatid  20120  scmatdmat  20140  mavmul0g  20178  1marepvmarrepid  20200  mdetunilem2  20238  gsummatr01lem3  20282  gsummatr01  20284  smadiadetlem3  20293  m2cpminvid2lem  20378  chpdmatlem2  20463  isopn3  20680  cnpval  20850  ptbasfi  21194  dfac14  21231  cnmptkk  21296  xkofvcn  21297  cnmptk1p  21298  cnmptk2  21299  xkocnv  21427  flfval  21604  ptcmplem3  21668  ptcmpg  21671  tmdmulg  21706  prdsxmslem2  22144  subgnm2  22248  nmoval  22329  fsum2cn  22482  pcovalg  22620  isclmp  22705  cphnm  22801  tchnmval  22836  ovolctb  23065  ioorcl  23151  uniioombllem2  23157  itg1addlem3  23271  itg1climres  23287  itg2uba  23316  itg2splitlem  23321  elcpn  23503  dvexp  23522  dvexp2  23523  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvlipcn  23561  dvlip2  23562  dveq0  23567  dv11cn  23568  lhop1lem  23580  lhop2  23582  lhop  23583  dvcvx  23587  ftc2ditglem  23612  itgsubstlem  23615  ig1pval  23736  elply2  23756  coeid2  23799  coemul  23812  taylthlem2  23932  ulmdvlem1  23958  mtest  23962  pserval2  23969  abelthlem1  23989  abelthlem3  23991  abelthlem8  23997  abelthlem9  23998  pige3  24073  0cxp  24212  leibpi  24469  igamgam  24575  mule1  24674  bposlem5  24813  lgsval3  24840  lgsdinn0  24870  dchrvmasumlem1  24984  dchrisum0flblem1  24997  rpvmasum2  25001  padicval  25106  axsegconlem1  25597  ax5seglem9  25617  axpasch  25621  axeuclidlem  25642  axcontlem2  25645  nbgraop  25952  nbgraop1  25954  constr1trl  26118  1pthon  26121  2pthlem2  26126  usgra2adedgwlkonALT  26144  constr3pthlem3  26185  wlkiswwlk2lem3  26221  wwlknred  26251  wwlkextproplem2  26270  clwwlkgt0  26299  clwlkisclwwlklem2a  26313  clwwlkf  26322  clwwlkext2edg  26330  wwlkext2clwwlk  26331  clwwisshclwwn  26336  erclwwlknsym  26354  erclwwlkntr  26355  el2spthonot0  26398  vdgrval  26423  extwwlkfablem1  26601  numclwwlkovf2ex  26613  numclwlk1lem2f1  26621  numclwwlk5lem  26638  grpoidinvlem4  26745  grpoinvval  26761  grpodivval  26773  ipval  26942  sspgval  26968  sspsval  26970  sspnval  26976  nmooval  27002  ipasslem1  27070  ipasslem4  27073  hial0  27343  hial02  27344  ocsh  27526  pjhval  27640  hosval  27983  homval  27984  hodval  27985  hfsval  27986  hfmval  27987  braval  28187  kbval  28197  eigvalval  28203  0hmop  28226  adj0  28237  lnopeq0i  28250  nmopcoi  28338  pjclem4  28442  pj3si  28450  hstoh  28475  strlem3a  28495  hstrlem3a  28503  mdexchi  28578  atcv0eq  28622  atcv1  28623  fpwrelmap  28896  smatfval  29189  measxun2  29600  measdivcstOLD  29614  measdivcst  29615  ddeval1  29624  ddeval0  29625  ballotlemfp1  29880  signswmnd  29960  signstfvneq0  29975  bnj1128  30312  subfacp1lem3  30418  subfacp1lem5  30420  cvmlift2lem3  30541  msubco  30682  altopthsn  31238  fnetr  31516  fnejoin2  31534  finxpreclem3  32406  finxpreclem5  32408  finxpreclem6  32409  curf  32557  curunc  32561  matunitlindf  32577  poimirlem4  32583  poimirlem25  32604  mblfinlem2  32617  mblfinlem3  32618  mbfresfi  32626  itg2addnclem  32631  itg2addnc  32634  ftc1anclem5  32659  isbnd3  32753  bndss  32755  grposnOLD  32851  ghomco  32860  lkrval  33393  pmapval  34061  polvalN  34209  watvalN  34297  ldilset  34413  ltrnset  34422  dilsetN  34458  trnsetN  34461  trlset  34466  trlval  34467  cdleme16b  34584  cdleme31fv1  34697  cdlemg1idlemN  34878  tgrpset  35051  tendoset  35065  erngset  35106  erngplus  35109  erngmul  35112  erngset-rN  35114  erngplus-rN  35117  dvaset  35311  dvaplusg  35315  dvamulr  35318  dvavadd  35321  dvavsca  35323  diafval  35338  dvhset  35388  dvhmulr  35393  dvhvadd  35399  dvhvsca  35408  docafvalN  35429  djafvalN  35441  dibfval  35448  dicfval  35482  dihfval  35538  dihval  35539  dihvalc  35540  dihvalb  35544  dochfval  35657  djhfval  35704  lcdval  35896  mapdfval  35934  mapdn0  35976  hvmapfval  36066  hdmap1fval  36104  hdmapfval  36137  hgmapfval  36196  pw2f1ocnv  36622  hbtlem7  36714  relexp0a  37027  ntrclscls00  37384  dvconstbi  37555  expgrowth  37556  addrfv  37694  subrfv  37695  mulvfv  37696  refsum2cnlem1  38219  limcperiod  38695  cncfiooiccre  38781  dvbdfbdioolem1  38818  itgioocnicc  38869  fourierdlem73  39072  fourierdlem82  39081  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  sqwvfoura  39121  etransclem46  39173  nnfoctbdjlem  39348  ovn0  39456  smflim  39663  afveu  39882  lighneallem3  40062  bgoldbwt  40199  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbnd  40225  ccats1pfxeqbi  40294  usgr2wlkspthlem2  40964  crctcshlem4  41023  wwlknp  41045  1wlkiswwlks2lem3  41068  wwlksnred  41098  wwlksnextproplem2  41116  wspthsnwspthsnon  41122  umgrwwlks2on  41161  clwlkclwwlklem2a  41207  clwwlksf  41222  clwwlksext2edg  41230  wwlksext2clwwlk  41231  clwwisshclwwsn  41236  erclwwlksnsym  41254  erclwwlksntr  41255  eupth2lem3lem3  41398  eucrct2eupth  41413  av-numclwwlkovf2ex  41517  av-numclwlk1lem2f1  41524  lmod0rng  41658  rnghmval  41681  lmodvsmdi  41957  lincdifsn  42007  lcoel0  42011  islindeps2  42066  blenn0  42165  nn0sumshdiglemA  42211  aacllem  42356