Theorem sylan9eq 2784

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

Syntax hints:   → wi 4   ∧ wa 395   = 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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  sylan9req  2785  sylan9eqr  2786  difeq12  4080  uneq12  4122  ineq12  4174  ssdifim  4232  ifeq12  4503  ifbi  4507  ifeq12da  4518  preq12  4695  prprc  4727  opeq12  4835  eqsnuniex  5311  opthwiener  5469  opthhausdorff0  5473  xpeq12  5656  sosn  5718  nfimad  6029  coi2  6224  funprg  6554  funtpg  6555  funcnvtp  6563  funcnvqp  6564  funimass1  6582  fimadmfoALT  6765  f1orescnv  6797  resdif  6803  fvmpt2  6961  fvmptnf  6972  fveqressseq  7033  oveq12  7378  cbvmpov  7464  ovmpog  7528  fvmpopr2d  7531  caofinvl  7665  eqopi  7983  el2mpocsbcl  8041  fmpoco  8051  mposn  8059  fsuppeqg  8132  supp0cosupp0  8164  imacosupp  8165  mpocurryd  8225  fvmpocurryd  8227  rdgsucmptf  8373  frsucmpt  8383  oevn0  8456  oa0r  8479  om1r  8484  oe1m  8486  omass  8521  oeoalem  8537  oeoa  8538  oeoe  8540  qseq12  8712  map0g  8834  xpcomco  9008  sbthlem4  9031  sbthlem5  9032  xpmapenlem  9085  phplem2  9146  unxpdomlem3  9175  funsnfsupp  9319  ordtypelem7  9453  ttrcltr  9645  cardennn  9912  dfac9  10066  alephsing  10205  axcc3  10367  ac6num  10408  konigthlem  10497  canthp1lem2  10582  ordpipq  10871  ltrnq  10908  addclprlem2  10946  mulclprlem  10948  prlem934  10962  prlem936  10976  mulcmpblnrlem  10999  addcnsr  11064  mulcnsr  11065  axcnre  11093  recex  11786  rpnnen1lem3  12914  rpnnen1lem5  12916  xaddpnf1  13162  xaddpnf2  13163  xaddmnf1  13164  xaddmnf2  13165  rexadd  13168  xnn0xaddcl  13171  xaddnemnf  13172  xaddnepnf  13173  xadddilem  13230  addmodlteq  13887  om2uzrani  13893  om2uzrdg  13897  seqf1olem2  13983  seqf1o  13984  modexp  14179  faclbnd4lem3  14236  hashunsng  14333  hashwrdn  14488  lsw1  14508  swrdfv  14589  swrdccat  14676  ccats1pfxeqbi  14683  revfv  14704  cshwsublen  14737  wrdlen2  14886  wrdl2exs2  14888  wwlktovf1  14899  relexp0  14965  relexpcnv  14977  shftcan1  15025  remul2  15072  immul2  15079  sumss  15666  geomulcvg  15818  fprodss  15890  binomfallfaclem2  15982  bpolylem  15990  ef0lem  16020  efieq1re  16143  rpnnen2lem1  16158  ruclem3  16177  dvdsnegb  16219  dvdscmul  16228  dvds2ln  16235  dvds2add  16236  dvds2sub  16237  gcdn0val  16444  rpmulgcd  16503  lcmn0val  16541  odzval  16738  pcval  16791  pcmpt  16839  prmreclem4  16866  1arithlem2  16871  vdwlem8  16935  ramcl2lem  16956  ramtcl  16957  ramtub  16959  ramcl2  16963  ramcl  16976  setsval  17113  prfcl  18140  curf1cl  18165  curfcl  18169  hofcl  18196  yonedalem4c  18214  psssdm  18517  grplactval  18950  mulgnn0gsum  18988  cntzval  19229  f1omvdco2  19354  pmtrfinv  19367  psgnunilem5  19400  odlem2  19445  gexlem2  19488  lsmvalx  19545  efgtval  19629  efgredlema  19646  vrgpval  19673  cyggex  19804  gsumcom2  19881  fincygsubgodd  20020  dvdsrtr  20253  rnghmval  20325  abvtrivd  20717  lmhmco  20926  reslmhm  20935  lvecinv  20999  zrhmulg  21395  znzrhval  21432  ocvval  21552  mplmon2  21944  subrgasclcl  21950  coe1fv  22067  coe1fzgsumdlem  22166  evl1gsumdlem  22219  mat1dimscm  22338  dmatid  22358  scmatdmat  22378  mavmul0g  22416  1marepvmarrepid  22438  mdetunilem2  22476  gsummatr01lem3  22520  gsummatr01  22522  smadiadetlem3  22531  m2cpminvid2lem  22617  chpdmatlem2  22702  isopn3  22929  cnpval  23099  ptbasfi  23444  dfac14  23481  cnmptkk  23546  xkofvcn  23547  cnmptk1p  23548  cnmptk2  23549  xkocnv  23677  flfval  23853  ptcmplem3  23917  ptcmpg  23920  tmdmulg  23955  prdsxmslem2  24393  subgnm2  24498  nmoval  24579  fsum2cn  24738  pcovalg  24888  isclmp  24973  cphnm  25069  tcphnmval  25105  ovolctb  25367  ioorcl  25454  uniioombllem2  25460  itg1addlem3  25575  itg1climres  25591  itg2uba  25620  itg2splitlem  25625  elcpn  25812  dvexp  25833  dvexp2  25834  rolle  25870  cmvth  25871  cmvthOLD  25872  mvth  25873  dvlip  25874  dvlipcn  25875  dvlip2  25876  dveq0  25881  dv11cn  25882  lhop1lem  25894  lhop2  25896  lhop  25897  dvcvx  25901  ftc2ditglem  25928  itgsubstlem  25931  ig1pval  26057  elply2  26077  coeid2  26120  coemul  26133  taylthlem2  26258  taylthlem2OLD  26259  ulmdvlem1  26285  mtest  26289  pserval2  26296  abelthlem1  26317  abelthlem3  26319  abelthlem8  26325  abelthlem9  26326  pige3ALT  26405  0cxp  26551  leibpi  26828  igamgam  26935  mule1  27034  bposlem5  27175  lgsval3  27202  lgsdinn0  27232  dchrvmasumlem1  27382  dchrisum0flblem1  27395  rpvmasum2  27399  padicval  27504  abssid  28119  abssnid  28121  axsegconlem1  28820  ax5seglem9  28840  axpasch  28844  axeuclidlem  28865  axcontlem2  28868  finsumvtxdg2ssteplem4  29452  usgr2wlkspthlem2  29661  crctcshlem4  29723  wwlknp  29746  wlkiswwlks2lem3  29774  wwlksnred  29795  wwlksnextproplem2  29813  umgrwwlks2on  29860  clwlkclwwlklem2a  29900  clwwisshclwwsn  29918  clwwlknlbonbgr1  29941  clwwlkn1loopb  29945  clwwlkf  29949  clwwlkext2edg  29958  wwlksext2clwwlk  29959  erclwwlknsym  29972  erclwwlkntr  29973  clwwlknon1  29999  clwwlknonex2  30011  eupth2lem3lem3  30132  eucrct2eupth  30147  fusgreghash2wspv  30237  2clwwlk2clwwlklem  30248  2clwwlk2clwwlk  30252  numclwwlk1lem2f1  30259  grpoidinvlem4  30409  grpoinvval  30425  grpodivval  30437  ipval  30605  sspgval  30631  sspsval  30633  sspnval  30639  nmooval  30665  ipasslem1  30733  ipasslem4  30736  hial0  31004  hial02  31005  ocsh  31185  pjhval  31299  hosval  31642  homval  31643  hodval  31644  hfsval  31645  hfmval  31646  braval  31846  kbval  31856  eigvalval  31862  0hmop  31885  adj0  31896  lnopeq0i  31909  nmopcoi  31997  pjclem4  32101  pj3si  32109  hstoh  32134  strlem3a  32154  hstrlem3a  32162  mdexchi  32237  atcv0eq  32281  atcv1  32282  fpwrelmap  32629  cycpmco2lem4  33059  cycpmco2lem5  33060  fxpgaval  33097  smatfval  33758  measxun2  34173  measdivcst  34187  measdivcstALTV  34188  ddeval1  34197  ddeval0  34198  ballotlemfp1  34456  signswmnd  34521  signstfvneq0  34536  signstfvc  34538  ftc2re  34562  itgexpif  34570  bnj1128  34953  subfacp1lem3  35142  subfacp1lem5  35144  cvmlift2lem3  35265  msubco  35491  altopthsn  35922  ditgeq12d  36183  fnetr  36312  fnejoin2  36330  bj-evalid  37037  finxpreclem3  37354  finxpreclem5  37356  finxpreclem6  37357  curf  37565  curunc  37569  matunitlindf  37585  poimirlem4  37591  poimirlem25  37612  mblfinlem2  37625  mblfinlem3  37626  mbfresfi  37633  itg2addnclem  37638  itg2addnc  37641  ftc1anclem5  37664  isbnd3  37751  bndss  37753  grposnOLD  37849  ghomco  37858  xrneq12  38342  lkrval  39054  pmapval  39724  polvalN  39872  watvalN  39960  ldilset  40076  ltrnset  40085  dilsetN  40120  trnsetN  40123  trlset  40128  trlval  40129  cdleme16b  40246  cdleme31fv1  40358  cdlemg1idlemN  40539  tgrpset  40712  tendoset  40726  erngset  40767  erngplus  40770  erngmul  40773  erngset-rN  40775  erngplus-rN  40778  dvaset  40972  dvaplusg  40976  dvamulr  40979  dvavadd  40982  dvavsca  40984  diafval  40998  dvhset  41048  dvhmulr  41053  dvhvadd  41059  dvhvsca  41068  docafvalN  41089  djafvalN  41101  dibfval  41108  dicfval  41142  dihfval  41198  dihval  41199  dihvalc  41200  dihvalb  41204  dochfval  41317  djhfval  41364  lcdval  41556  mapdfval  41594  mapdn0  41636  hvmapfval  41726  hdmap1fval  41763  hdmapfval  41794  hgmapfval  41853  fmpocos  42195  sn-it0e0  42377  zaddcomlem  42424  pw2f1ocnv  42999  hbtlem7  43087  relexp0a  43678  ntrclscls00  44028  dvconstbi  44296  expgrowth  44297  addrfv  44431  subrfv  44432  mulvfv  44433  refsum2cnlem1  45004  limcperiod  45599  cncfiooiccre  45866  dvbdfbdioolem1  45899  itgioocnicc  45948  fourierdlem73  46150  fourierdlem82  46159  fourierdlem94  46171  fourierdlem103  46180  fourierdlem104  46181  fourierdlem113  46190  sqwvfoura  46199  etransclem46  46251  nnfoctbdjlem  46426  ovn0  46537  smflim  46748  afveu  47127  afv2eu  47212  fvmptrabdm  47267  imasetpreimafvbijlemfo  47379  lighneallem3  47581  mogoldbblem  47694  fpprel2  47715  sbgoldbwt  47751  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  bgoldbtbnd  47783  grimco  47862  cycl3grtri  47919  lmod0rng  48190  lmodvsmdi  48340  lincdifsn  48386  lcoel0  48390  islindeps2  48445  blenn0  48535  nn0sumshdiglemA  48581  itcoval0mpt  48628  rrx2plordisom  48685  nelsubclem  49029  aacllem  49763