Theorem sylan9eq 2853

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  sylan9req  2854  sylan9eqr  2855  difeq12  4045  uneq12  4085  ineq12  4134  ssdifim  4189  ifeq12  4442  ifbi  4446  ifeq12da  4457  preq12  4631  prprc  4663  opeq12  4767  opthwiener  5369  opthhausdorff0  5373  xpeq12  5544  sosn  5602  nfimad  5905  coi2  6083  funprg  6378  funtpg  6379  funcnvtp  6387  funcnvqp  6388  funimass1  6406  fimadmfoALT  6576  f1orescnv  6605  resdif  6610  fvmpt2  6756  fvmptnf  6767  fveqressseq  6824  oveq12  7144  cbvmpov  7228  ovmpog  7288  fvmpopr2d  7290  caofinvl  7416  eqopi  7707  el2mpocsbcl  7763  fmpoco  7773  mposn  7781  supp0cosupp0  7855  supp0cosupp0OLD  7856  imacosupp  7857  mpocurryd  7918  fvmpocurryd  7920  wrecseq123  7931  rdgsucmptf  8047  frsucmpt  8056  oevn0  8123  oa0r  8146  om1r  8152  oe1m  8154  omass  8189  oeoalem  8205  oeoa  8206  oeoe  8208  qseq12  8330  map0g  8431  xpcomco  8590  sbthlem4  8614  sbthlem5  8615  xpmapenlem  8668  phplem3  8682  phplem4  8683  unxpdomlem3  8708  funsnfsupp  8841  ordtypelem7  8972  cardennn  9396  dfac9  9547  alephsing  9687  axcc3  9849  ac6num  9890  konigthlem  9979  canthp1lem2  10064  ordpipq  10353  ltrnq  10390  addclprlem2  10428  mulclprlem  10430  prlem934  10444  prlem936  10458  mulcmpblnrlem  10481  addcnsr  10546  mulcnsr  10547  axcnre  10575  recex  11261  rpnnen1lem3  12366  rpnnen1lem5  12368  xaddpnf1  12607  xaddpnf2  12608  xaddmnf1  12609  xaddmnf2  12610  rexadd  12613  xnn0xaddcl  12616  xaddnemnf  12617  xaddnepnf  12618  xadddilem  12675  addmodlteq  13309  om2uzrani  13315  om2uzrdg  13319  seqf1olem2  13406  seqf1o  13407  modexp  13595  faclbnd4lem3  13651  hashunsng  13749  hashwrdn  13890  lsw1  13910  swrdfv  14001  swrdccat  14088  ccats1pfxeqbi  14095  revfv  14116  cshwsublen  14149  wrdlen2  14297  wrdl2exs2  14299  wwlktovf1  14312  relexp0  14374  relexpcnv  14386  shftcan1  14434  remul2  14481  immul2  14488  sumss  15073  geomulcvg  15224  fprodss  15294  binomfallfaclem2  15386  bpolylem  15394  ef0lem  15424  efieq1re  15544  rpnnen2lem1  15559  ruclem3  15578  dvdsnegb  15619  dvdscmul  15628  dvds2ln  15634  dvds2add  15635  dvds2sub  15636  gcdn0val  15837  rpmulgcd  15896  lcmn0val  15929  odzval  16118  pcval  16171  pcmpt  16218  prmreclem4  16245  1arithlem2  16250  vdwlem8  16314  ramcl2lem  16335  ramtcl  16336  ramtub  16338  ramcl2  16342  ramcl  16355  setsval  16505  prfcl  17445  curf1cl  17470  curfcl  17474  hofcl  17501  yonedalem4c  17519  psssdm  17818  grplactval  18193  mulgnn0gsum  18226  cntzval  18443  f1omvdco2  18568  pmtrfinv  18581  psgnunilem5  18614  odlem2  18659  gexlem2  18699  lsmvalx  18756  efgtval  18841  efgredlema  18858  vrgpval  18885  cyggex  19011  gsumcom2  19088  fincygsubgodd  19227  dvdsrtr  19398  abvtrivd  19604  lmhmco  19808  reslmhm  19817  lvecinv  19878  zrhmulg  20203  znzrhval  20238  ocvval  20356  mplmon2  20732  subrgasclcl  20738  coe1fv  20835  coe1fzgsumdlem  20930  evl1gsumdlem  20980  mat1dimscm  21080  dmatid  21100  scmatdmat  21120  mavmul0g  21158  1marepvmarrepid  21180  mdetunilem2  21218  gsummatr01lem3  21262  gsummatr01  21264  smadiadetlem3  21273  m2cpminvid2lem  21359  chpdmatlem2  21444  isopn3  21671  cnpval  21841  ptbasfi  22186  dfac14  22223  cnmptkk  22288  xkofvcn  22289  cnmptk1p  22290  cnmptk2  22291  xkocnv  22419  flfval  22595  ptcmplem3  22659  ptcmpg  22662  tmdmulg  22697  prdsxmslem2  23136  subgnm2  23240  nmoval  23321  fsum2cn  23476  pcovalg  23617  isclmp  23702  cphnm  23798  tcphnmval  23833  ovolctb  24094  ioorcl  24181  uniioombllem2  24187  itg1addlem3  24302  itg1climres  24318  itg2uba  24347  itg2splitlem  24352  elcpn  24537  dvexp  24556  dvexp2  24557  rolle  24593  cmvth  24594  mvth  24595  dvlip  24596  dvlipcn  24597  dvlip2  24598  dveq0  24603  dv11cn  24604  lhop1lem  24616  lhop2  24618  lhop  24619  dvcvx  24623  ftc2ditglem  24648  itgsubstlem  24651  ig1pval  24773  elply2  24793  coeid2  24836  coemul  24849  taylthlem2  24969  ulmdvlem1  24995  mtest  24999  pserval2  25006  abelthlem1  25026  abelthlem3  25028  abelthlem8  25034  abelthlem9  25035  pige3ALT  25112  0cxp  25257  leibpi  25528  igamgam  25634  mule1  25733  bposlem5  25872  lgsval3  25899  lgsdinn0  25929  dchrvmasumlem1  26079  dchrisum0flblem1  26092  rpvmasum2  26096  padicval  26201  axsegconlem1  26711  ax5seglem9  26731  axpasch  26735  axeuclidlem  26756  axcontlem2  26759  finsumvtxdg2ssteplem4  27338  usgr2wlkspthlem2  27547  crctcshlem4  27606  wwlknp  27629  wlkiswwlks2lem3  27657  wwlksnred  27678  wwlksnextproplem2  27696  umgrwwlks2on  27743  clwlkclwwlklem2a  27783  clwwisshclwwsn  27801  clwwlknlbonbgr1  27824  clwwlkn1loopb  27828  clwwlkf  27832  clwwlkext2edg  27841  wwlksext2clwwlk  27842  erclwwlknsym  27855  erclwwlkntr  27856  clwwlknon1  27882  clwwlknonex2  27894  eupth2lem3lem3  28015  eucrct2eupth  28030  fusgreghash2wspv  28120  2clwwlk2clwwlklem  28131  2clwwlk2clwwlk  28135  numclwwlk1lem2f1  28142  grpoidinvlem4  28290  grpoinvval  28306  grpodivval  28318  ipval  28486  sspgval  28512  sspsval  28514  sspnval  28520  nmooval  28546  ipasslem1  28614  ipasslem4  28617  hial0  28885  hial02  28886  ocsh  29066  pjhval  29180  hosval  29523  homval  29524  hodval  29525  hfsval  29526  hfmval  29527  braval  29727  kbval  29737  eigvalval  29743  0hmop  29766  adj0  29777  lnopeq0i  29790  nmopcoi  29878  pjclem4  29982  pj3si  29990  hstoh  30015  strlem3a  30035  hstrlem3a  30043  mdexchi  30118  atcv0eq  30162  atcv1  30163  fpwrelmap  30495  cycpmco2lem4  30821  cycpmco2lem5  30822  smatfval  31148  measxun2  31579  measdivcst  31593  measdivcstALTV  31594  ddeval1  31603  ddeval0  31604  ballotlemfp1  31859  signswmnd  31937  signstfvneq0  31952  signstfvc  31954  ftc2re  31979  itgexpif  31987  bnj1128  32372  subfacp1lem3  32542  subfacp1lem5  32544  cvmlift2lem3  32665  msubco  32891  altopthsn  33535  fnetr  33812  fnejoin2  33830  bj-evalid  34491  finxpreclem3  34810  finxpreclem5  34812  finxpreclem6  34813  curf  35035  curunc  35039  matunitlindf  35055  poimirlem4  35061  poimirlem25  35082  mblfinlem2  35095  mblfinlem3  35096  mbfresfi  35103  itg2addnclem  35108  itg2addnc  35111  ftc1anclem5  35134  isbnd3  35222  bndss  35224  grposnOLD  35320  ghomco  35329  xrneq12  35795  lkrval  36384  pmapval  37053  polvalN  37201  watvalN  37289  ldilset  37405  ltrnset  37414  dilsetN  37449  trnsetN  37452  trlset  37457  trlval  37458  cdleme16b  37575  cdleme31fv1  37687  cdlemg1idlemN  37868  tgrpset  38041  tendoset  38055  erngset  38096  erngplus  38099  erngmul  38102  erngset-rN  38104  erngplus-rN  38107  dvaset  38301  dvaplusg  38305  dvamulr  38308  dvavadd  38311  dvavsca  38313  diafval  38327  dvhset  38377  dvhmulr  38382  dvhvadd  38388  dvhvsca  38397  docafvalN  38418  djafvalN  38430  dibfval  38437  dicfval  38471  dihfval  38527  dihval  38528  dihvalc  38529  dihvalb  38533  dochfval  38646  djhfval  38693  lcdval  38885  mapdfval  38923  mapdn0  38965  hvmapfval  39055  hdmap1fval  39092  hdmapfval  39123  hgmapfval  39182  sn-it0e0  39552  pw2f1ocnv  39978  hbtlem7  40069  relexp0a  40417  ntrclscls00  40769  dvconstbi  41038  expgrowth  41039  addrfv  41173  subrfv  41174  mulvfv  41175  refsum2cnlem1  41666  limcperiod  42270  cncfiooiccre  42537  dvbdfbdioolem1  42570  itgioocnicc  42619  fourierdlem73  42821  fourierdlem82  42830  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem113  42861  sqwvfoura  42870  etransclem46  42922  nnfoctbdjlem  43094  ovn0  43205  smflim  43410  afveu  43709  afv2eu  43794  fvmptrabdm  43849  imasetpreimafvbijlemfo  43922  lighneallem3  44125  mogoldbblem  44238  fpprel2  44259  sbgoldbwt  44295  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbnd  44327  lmod0rng  44492  rnghmval  44515  lmodvsmdi  44784  lincdifsn  44833  lcoel0  44837  islindeps2  44892  blenn0  44987  nn0sumshdiglemA  45033  itcoval0mpt  45080  rrx2plordisom  45137  aacllem  45329