Theorem sylan9eq 2786

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

Syntax hints:   → wi 4   ∧ wa 395   = 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:  sylan9req  2787  sylan9eqr  2788  difeq12  4068  uneq12  4110  ineq12  4162  ssdifim  4220  ifeq12  4491  ifbi  4495  ifeq12da  4506  preq12  4685  prprc  4717  opeq12  4824  eqsnuniex  5297  opthwiener  5452  opthhausdorff0  5456  xpeq12  5639  sosn  5701  nfimad  6017  coi2  6211  funprg  6535  funtpg  6536  funcnvtp  6544  funcnvqp  6545  funimass1  6563  fimadmfoALT  6746  f1orescnv  6778  resdif  6784  fvmpt2  6940  fvmptnf  6951  fveqressseq  7012  oveq12  7355  cbvmpov  7441  ovmpog  7505  fvmpopr2d  7508  caofinvl  7642  eqopi  7957  el2mpocsbcl  8015  fmpoco  8025  mposn  8033  fsuppeqg  8106  supp0cosupp0  8138  imacosupp  8139  mpocurryd  8199  fvmpocurryd  8201  rdgsucmptf  8347  frsucmpt  8357  oevn0  8430  oa0r  8453  om1r  8458  oe1m  8460  omass  8495  oeoalem  8511  oeoa  8512  oeoe  8514  qseq12  8686  map0g  8808  xpcomco  8980  sbthlem4  9003  sbthlem5  9004  xpmapenlem  9057  phplem2  9114  unxpdomlem3  9142  funsnfsupp  9276  ordtypelem7  9410  ttrcltr  9606  cardennn  9876  dfac9  10028  alephsing  10167  axcc3  10329  ac6num  10370  konigthlem  10459  canthp1lem2  10544  ordpipq  10833  ltrnq  10870  addclprlem2  10908  mulclprlem  10910  prlem934  10924  prlem936  10938  mulcmpblnrlem  10961  addcnsr  11026  mulcnsr  11027  axcnre  11055  recex  11749  rpnnen1lem3  12877  rpnnen1lem5  12879  xaddpnf1  13125  xaddpnf2  13126  xaddmnf1  13127  xaddmnf2  13128  rexadd  13131  xnn0xaddcl  13134  xaddnemnf  13135  xaddnepnf  13136  xadddilem  13193  addmodlteq  13853  om2uzrani  13859  om2uzrdg  13863  seqf1olem2  13949  seqf1o  13950  modexp  14145  faclbnd4lem3  14202  hashunsng  14299  hashwrdn  14454  lsw1  14474  swrdfv  14556  swrdccat  14642  ccats1pfxeqbi  14649  revfv  14670  cshwsublen  14703  wrdlen2  14851  wrdl2exs2  14853  wwlktovf1  14864  relexp0  14930  relexpcnv  14942  shftcan1  14990  remul2  15037  immul2  15044  sumss  15631  geomulcvg  15783  fprodss  15855  binomfallfaclem2  15947  bpolylem  15955  ef0lem  15985  efieq1re  16108  rpnnen2lem1  16123  ruclem3  16142  dvdsnegb  16184  dvdscmul  16193  dvds2ln  16200  dvds2add  16201  dvds2sub  16202  gcdn0val  16409  rpmulgcd  16468  lcmn0val  16506  odzval  16703  pcval  16756  pcmpt  16804  prmreclem4  16831  1arithlem2  16836  vdwlem8  16900  ramcl2lem  16921  ramtcl  16922  ramtub  16924  ramcl2  16928  ramcl  16941  setsval  17078  prfcl  18109  curf1cl  18134  curfcl  18138  hofcl  18165  yonedalem4c  18183  psssdm  18488  chneq12  18520  grplactval  18955  mulgnn0gsum  18993  cntzval  19233  f1omvdco2  19360  pmtrfinv  19373  psgnunilem5  19406  odlem2  19451  gexlem2  19494  lsmvalx  19551  efgtval  19635  efgredlema  19652  vrgpval  19679  cyggex  19810  gsumcom2  19887  fincygsubgodd  20026  dvdsrtr  20286  rnghmval  20358  abvtrivd  20747  lmhmco  20977  reslmhm  20986  lvecinv  21050  zrhmulg  21446  znzrhval  21483  ocvval  21604  mplmon2  21996  subrgasclcl  22002  coe1fv  22119  coe1fzgsumdlem  22218  evl1gsumdlem  22271  mat1dimscm  22390  dmatid  22410  scmatdmat  22430  mavmul0g  22468  1marepvmarrepid  22490  mdetunilem2  22528  gsummatr01lem3  22572  gsummatr01  22574  smadiadetlem3  22583  m2cpminvid2lem  22669  chpdmatlem2  22754  isopn3  22981  cnpval  23151  ptbasfi  23496  dfac14  23533  cnmptkk  23598  xkofvcn  23599  cnmptk1p  23600  cnmptk2  23601  xkocnv  23729  flfval  23905  ptcmplem3  23969  ptcmpg  23972  tmdmulg  24007  prdsxmslem2  24444  subgnm2  24549  nmoval  24630  fsum2cn  24789  pcovalg  24939  isclmp  25024  cphnm  25120  tcphnmval  25156  ovolctb  25418  ioorcl  25505  uniioombllem2  25511  itg1addlem3  25626  itg1climres  25642  itg2uba  25671  itg2splitlem  25676  elcpn  25863  dvexp  25884  dvexp2  25885  rolle  25921  cmvth  25922  cmvthOLD  25923  mvth  25924  dvlip  25925  dvlipcn  25926  dvlip2  25927  dveq0  25932  dv11cn  25933  lhop1lem  25945  lhop2  25947  lhop  25948  dvcvx  25952  ftc2ditglem  25979  itgsubstlem  25982  ig1pval  26108  elply2  26128  coeid2  26171  coemul  26184  taylthlem2  26309  taylthlem2OLD  26310  ulmdvlem1  26336  mtest  26340  pserval2  26347  abelthlem1  26368  abelthlem3  26370  abelthlem8  26376  abelthlem9  26377  pige3ALT  26456  0cxp  26602  leibpi  26879  igamgam  26986  mule1  27085  bposlem5  27226  lgsval3  27253  lgsdinn0  27283  dchrvmasumlem1  27433  dchrisum0flblem1  27446  rpvmasum2  27450  padicval  27555  abssid  28179  abssnid  28181  axsegconlem1  28895  ax5seglem9  28915  axpasch  28919  axeuclidlem  28940  axcontlem2  28943  finsumvtxdg2ssteplem4  29527  usgr2wlkspthlem2  29736  crctcshlem4  29798  wwlknp  29821  wlkiswwlks2lem3  29849  wwlksnred  29870  wwlksnextproplem2  29888  usgrwwlks2on  29936  umgrwwlks2on  29937  clwlkclwwlklem2a  29978  clwwisshclwwsn  29996  clwwlknlbonbgr1  30019  clwwlkn1loopb  30023  clwwlkf  30027  clwwlkext2edg  30036  wwlksext2clwwlk  30037  erclwwlknsym  30050  erclwwlkntr  30051  clwwlknon1  30077  clwwlknonex2  30089  eupth2lem3lem3  30210  eucrct2eupth  30225  fusgreghash2wspv  30315  2clwwlk2clwwlklem  30326  2clwwlk2clwwlk  30330  numclwwlk1lem2f1  30337  grpoidinvlem4  30487  grpoinvval  30503  grpodivval  30515  ipval  30683  sspgval  30709  sspsval  30711  sspnval  30717  nmooval  30743  ipasslem1  30811  ipasslem4  30814  hial0  31082  hial02  31083  ocsh  31263  pjhval  31377  hosval  31720  homval  31721  hodval  31722  hfsval  31723  hfmval  31724  braval  31924  kbval  31934  eigvalval  31940  0hmop  31963  adj0  31974  lnopeq0i  31987  nmopcoi  32075  pjclem4  32179  pj3si  32187  hstoh  32212  strlem3a  32232  hstrlem3a  32240  mdexchi  32315  atcv0eq  32359  atcv1  32360  fpwrelmap  32716  cycpmco2lem4  33098  cycpmco2lem5  33099  fxpgaval  33136  smatfval  33808  measxun2  34223  measdivcst  34237  measdivcstALTV  34238  ddeval1  34247  ddeval0  34248  ballotlemfp1  34505  signswmnd  34570  signstfvneq0  34585  signstfvc  34587  ftc2re  34611  itgexpif  34619  bnj1128  35002  subfacp1lem3  35226  subfacp1lem5  35228  cvmlift2lem3  35349  msubco  35575  altopthsn  36003  ditgeq12d  36264  fnetr  36393  fnejoin2  36411  bj-evalid  37118  finxpreclem3  37435  finxpreclem5  37437  finxpreclem6  37438  curf  37646  curunc  37650  matunitlindf  37666  poimirlem4  37672  poimirlem25  37693  mblfinlem2  37706  mblfinlem3  37707  mbfresfi  37714  itg2addnclem  37719  itg2addnc  37722  ftc1anclem5  37745  isbnd3  37832  bndss  37834  grposnOLD  37930  ghomco  37939  xrneq12  38423  lkrval  39135  pmapval  39804  polvalN  39952  watvalN  40040  ldilset  40156  ltrnset  40165  dilsetN  40200  trnsetN  40203  trlset  40208  trlval  40209  cdleme16b  40326  cdleme31fv1  40438  cdlemg1idlemN  40619  tgrpset  40792  tendoset  40806  erngset  40847  erngplus  40850  erngmul  40853  erngset-rN  40855  erngplus-rN  40858  dvaset  41052  dvaplusg  41056  dvamulr  41059  dvavadd  41062  dvavsca  41064  diafval  41078  dvhset  41128  dvhmulr  41133  dvhvadd  41139  dvhvsca  41148  docafvalN  41169  djafvalN  41181  dibfval  41188  dicfval  41222  dihfval  41278  dihval  41279  dihvalc  41280  dihvalb  41284  dochfval  41397  djhfval  41444  lcdval  41636  mapdfval  41674  mapdn0  41716  hvmapfval  41806  hdmap1fval  41843  hdmapfval  41874  hgmapfval  41933  fmpocos  42275  sn-it0e0  42457  zaddcomlem  42504  pw2f1ocnv  43078  hbtlem7  43166  relexp0a  43757  ntrclscls00  44107  dvconstbi  44375  expgrowth  44376  addrfv  44509  subrfv  44510  mulvfv  44511  refsum2cnlem1  45082  limcperiod  45676  cncfiooiccre  45941  dvbdfbdioolem1  45974  itgioocnicc  46023  fourierdlem73  46225  fourierdlem82  46234  fourierdlem94  46246  fourierdlem103  46255  fourierdlem104  46256  fourierdlem113  46265  sqwvfoura  46274  etransclem46  46326  nnfoctbdjlem  46501  ovn0  46612  smflim  46823  afveu  47192  afv2eu  47277  fvmptrabdm  47332  imasetpreimafvbijlemfo  47444  lighneallem3  47646  mogoldbblem  47759  fpprel2  47780  sbgoldbwt  47816  nnsum4primeseven  47839  nnsum4primesevenALTV  47840  bgoldbtbnd  47848  grimco  47928  cycl3grtri  47986  lmod0rng  48268  lmodvsmdi  48418  lincdifsn  48464  lcoel0  48468  islindeps2  48523  blenn0  48613  nn0sumshdiglemA  48659  itcoval0mpt  48706  rrx2plordisom  48763  nelsubclem  49107  aacllem  49841