Theorem sylan9eq 2829

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 2794	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 587	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-9 2060  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-cleq 2766

This theorem is referenced by:  sylan9req  2830  sylan9eqr  2831  difeq12  3979  uneq12  4018  ineq12  4066  ssdifim  4121  ifeq12  4362  ifbi  4366  ifeq12da  4377  preq12  4542  prprc  4574  opeq12  4676  opthwiener  5257  opthhausdorff0  5261  xpeq12  5429  sosn  5485  nfimad  5777  coi2  5953  funprg  6239  funtpg  6240  funcnvtp  6248  funcnvqp  6249  funimass1  6267  fimadmfoALT  6428  f1orescnv  6457  resdif  6462  fvmpt2  6604  fvmptnf  6615  fveqressseq  6671  oveq12  6984  cbvmpov  7064  ovmpog  7124  caofinvl  7253  eqopi  7536  el2mpocsbcl  7587  fmpoco  7597  mposn  7605  supp0cosupp0  7674  supp0cosupp0OLD  7675  imacosupp  7676  mpocurryd  7737  fvmpocurryd  7739  wrecseq123  7750  rdgsucmptf  7867  frsucmpt  7876  oevn0  7941  oa0r  7964  om1r  7969  oe1m  7971  omass  8006  oeoalem  8022  oeoa  8023  oeoe  8025  qseq12  8146  map0g  8246  xpcomco  8402  sbthlem4  8425  sbthlem5  8426  xpmapenlem  8479  phplem3  8493  phplem4  8494  unxpdomlem3  8518  funsnfsupp  8651  ordtypelem7  8782  cardennn  9205  dfac9  9355  alephsing  9495  axcc3  9657  ac6num  9698  konigthlem  9787  canthp1lem2  9872  ordpipq  10161  ltrnq  10198  addclprlem2  10236  mulclprlem  10238  prlem934  10252  prlem936  10266  mulcmpblnrlem  10289  addcnsr  10354  mulcnsr  10355  axcnre  10383  recex  11072  rpnnen1lem3  12192  rpnnen1lem5  12194  xaddpnf1  12435  xaddpnf2  12436  xaddmnf1  12437  xaddmnf2  12438  rexadd  12441  xnn0xaddcl  12444  xaddnemnf  12445  xaddnepnf  12446  xadddilem  12502  addmodlteq  13128  om2uzrani  13134  om2uzrdg  13138  seqf1olem2  13224  seqf1o  13225  modexp  13413  faclbnd4lem3  13469  hashunsng  13565  hashwrdn  13708  lsw1  13729  swrdfv  13812  swrdccat  13937  swrdccatOLD  13938  ccats1pfxeqbi  13948  ccats1swrdeqbiOLD  13949  revfv  13981  cshwsublen  14019  wrdlen2  14167  wrdl2exs2  14169  wwlktovf1  14181  relexp0  14242  relexpcnv  14254  shftcan1  14302  remul2  14349  immul2  14356  sumss  14940  geomulcvg  15091  fprodss  15161  binomfallfaclem2  15253  bpolylem  15261  ef0lem  15291  efieq1re  15411  rpnnen2lem1  15426  ruclem3  15445  dvdsnegb  15486  dvdscmul  15495  dvds2ln  15501  dvds2add  15502  dvds2sub  15503  gcdn0val  15706  rpmulgcd  15761  lcmn0val  15794  odzval  15983  pcval  16036  pcmpt  16083  prmreclem4  16110  1arithlem2  16115  vdwlem8  16179  ramcl2lem  16200  ramtcl  16201  ramtub  16203  ramcl2  16207  ramcl  16220  setsval  16368  prfcl  17324  curf1cl  17349  curfcl  17353  hofcl  17380  yonedalem4c  17398  psssdm  17697  grplactval  18001  cntzval  18235  f1omvdco2  18350  pmtrfinv  18363  psgnunilem5  18396  psgnunilem5OLD  18397  odlem2  18442  gexlem2  18481  lsmvalx  18538  efgtval  18620  efgredlema  18638  vrgpval  18666  cyggex  18785  gsumcom2  18861  dvdsrtr  19138  abvtrivd  19346  lmhmco  19550  reslmhm  19559  lvecinv  19620  mplmon2  19999  subrgasclcl  20005  coe1fv  20093  coe1fzgsumdlem  20188  evl1gsumdlem  20237  zrhmulg  20375  znzrhval  20411  ocvval  20529  mat1dimscm  20804  dmatid  20824  scmatdmat  20844  mavmul0g  20882  1marepvmarrepid  20904  mdetunilem2  20942  gsummatr01lem3  20986  gsummatr01  20988  smadiadetlem3  20997  m2cpminvid2lem  21082  chpdmatlem2  21167  isopn3  21394  cnpval  21564  ptbasfi  21909  dfac14  21946  cnmptkk  22011  xkofvcn  22012  cnmptk1p  22013  cnmptk2  22014  xkocnv  22142  flfval  22318  ptcmplem3  22382  ptcmpg  22385  tmdmulg  22420  prdsxmslem2  22858  subgnm2  22962  nmoval  23043  fsum2cn  23198  pcovalg  23335  isclmp  23420  cphnm  23516  tcphnmval  23551  ovolctb  23810  ioorcl  23897  uniioombllem2  23903  itg1addlem3  24018  itg1climres  24034  itg2uba  24063  itg2splitlem  24068  elcpn  24250  dvexp  24269  dvexp2  24270  rolle  24306  cmvth  24307  mvth  24308  dvlip  24309  dvlipcn  24310  dvlip2  24311  dveq0  24316  dv11cn  24317  lhop1lem  24329  lhop2  24331  lhop  24332  dvcvx  24336  ftc2ditglem  24361  itgsubstlem  24364  ig1pval  24485  elply2  24505  coeid2  24548  coemul  24561  taylthlem2  24681  ulmdvlem1  24707  mtest  24711  pserval2  24718  abelthlem1  24738  abelthlem3  24740  abelthlem8  24746  abelthlem9  24747  pige3ALT  24824  0cxp  24966  leibpi  25238  igamgam  25344  mule1  25443  bposlem5  25582  lgsval3  25609  lgsdinn0  25639  dchrvmasumlem1  25789  dchrisum0flblem1  25802  rpvmasum2  25806  padicval  25911  axsegconlem1  26422  ax5seglem9  26442  axpasch  26446  axeuclidlem  26467  axcontlem2  26470  finsumvtxdg2ssteplem4  27049  usgr2wlkspthlem2  27263  crctcshlem4  27322  wwlknp  27345  wlkiswwlks2lem3  27373  wwlksnred  27395  wwlksnredOLD  27396  wwlksnextproplem2  27427  wwlksnextproplem2OLD  27428  umgrwwlks2on  27479  clwlkclwwlklem2a  27520  clwwisshclwwsn  27547  clwwlknlbonbgr1  27570  clwwlkn1loopb  27575  clwwlkfOLD  27580  clwwlkf  27585  clwwlkext2edg  27595  erclwwlknsym  27610  erclwwlkntr  27611  clwwlknon1  27641  clwwlknonex2  27653  eupth2lem3lem3  27776  eucrct2eupthOLD  27792  eucrct2eupth  27793  fusgreghash2wspv  27885  2clwwlk2clwwlklem  27899  2clwwlk2clwwlk  27903  2clwwlk2clwwlkOLD  27904  numclwwlk1lem2f1  27915  numclwwlk1lem2f1OLD  27920  grpoidinvlem4  28077  grpoinvval  28093  grpodivval  28105  ipval  28273  sspgval  28299  sspsval  28301  sspnval  28307  nmooval  28333  ipasslem1  28401  ipasslem4  28404  hial0  28674  hial02  28675  ocsh  28857  pjhval  28971  hosval  29314  homval  29315  hodval  29316  hfsval  29317  hfmval  29318  braval  29518  kbval  29528  eigvalval  29534  0hmop  29557  adj0  29568  lnopeq0i  29581  nmopcoi  29669  pjclem4  29773  pj3si  29781  hstoh  29806  strlem3a  29826  hstrlem3a  29834  mdexchi  29909  atcv0eq  29953  atcv1  29954  fpwrelmap  30246  smatfval  30735  measxun2  31147  measdivcstOLD  31161  measdivcst  31162  ddeval1  31171  ddeval0  31172  ballotlemfp1  31428  signswmnd  31506  signstfvneq0  31522  ftc2re  31550  itgexpif  31558  bnj1128  31940  subfacp1lem3  32047  subfacp1lem5  32049  cvmlift2lem3  32170  msubco  32331  altopthsn  32976  fnetr  33253  fnejoin2  33271  bj-evalid  33909  finxpreclem3  34148  finxpreclem5  34150  finxpreclem6  34151  curf  34344  curunc  34348  matunitlindf  34364  poimirlem4  34370  poimirlem25  34391  mblfinlem2  34404  mblfinlem3  34405  mbfresfi  34412  itg2addnclem  34417  itg2addnc  34420  ftc1anclem5  34445  isbnd3  34537  bndss  34539  grposnOLD  34635  ghomco  34644  xrneq12  35113  lkrval  35702  pmapval  36371  polvalN  36519  watvalN  36607  ldilset  36723  ltrnset  36732  dilsetN  36767  trnsetN  36770  trlset  36775  trlval  36776  cdleme16b  36893  cdleme31fv1  37005  cdlemg1idlemN  37186  tgrpset  37359  tendoset  37373  erngset  37414  erngplus  37417  erngmul  37420  erngset-rN  37422  erngplus-rN  37425  dvaset  37619  dvaplusg  37623  dvamulr  37626  dvavadd  37629  dvavsca  37631  diafval  37645  dvhset  37695  dvhmulr  37700  dvhvadd  37706  dvhvsca  37715  docafvalN  37736  djafvalN  37748  dibfval  37755  dicfval  37789  dihfval  37845  dihval  37846  dihvalc  37847  dihvalb  37851  dochfval  37964  djhfval  38011  lcdval  38203  mapdfval  38241  mapdn0  38283  hvmapfval  38373  hdmap1fval  38410  hdmapfval  38441  hgmapfval  38500  pw2f1ocnv  39064  hbtlem7  39155  relexp0a  39458  ntrclscls00  39813  fincygsubgodd  40081  dvconstbi  40116  expgrowth  40117  addrfv  40254  subrfv  40255  mulvfv  40256  refsum2cnlem1  40747  limcperiod  41370  cncfiooiccre  41638  dvbdfbdioolem1  41673  itgioocnicc  41722  fourierdlem73  41925  fourierdlem82  41934  fourierdlem94  41946  fourierdlem103  41955  fourierdlem104  41956  fourierdlem113  41965  sqwvfoura  41974  etransclem46  42026  nnfoctbdjlem  42198  ovn0  42309  smflim  42514  afveu  42788  afv2eu  42873  fvmptrabdm  42928  lighneallem3  43170  mogoldbblem  43283  fpprel2  43304  sbgoldbwt  43340  nnsum4primeseven  43363  nnsum4primesevenALTV  43364  bgoldbtbnd  43372  lmod0rng  43533  rnghmval  43556  lmodvsmdi  43826  lincdifsn  43876  lcoel0  43880  islindeps2  43935  blenn0  44031  nn0sumshdiglemA  44077  rrx2plordisom  44108  aacllem  44299