Theorem sylan9eq 2791

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  sylan9req  2792  sylan9eqr  2793  difeq12  4061  uneq12  4103  ineq12  4155  ssdifim  4213  ifeq12  4485  ifbi  4489  ifeq12da  4500  preq12  4679  prprc  4711  opeq12  4818  eqsnuniex  5303  opthwiener  5468  opthhausdorff0  5472  xpeq12  5656  sosn  5718  nfimad  6034  coi2  6228  funprg  6552  funtpg  6553  funcnvtp  6561  funcnvqp  6562  funimass1  6580  fimadmfoALT  6763  f1orescnv  6795  resdif  6801  fvmpt2  6959  fvmptnf  6970  fveqressseq  7031  oveq12  7376  cbvmpov  7462  ovmpog  7526  fvmpopr2d  7529  caofinvl  7663  eqopi  7978  el2mpocsbcl  8035  fmpoco  8045  mposn  8053  fsuppeqg  8126  supp0cosupp0  8158  imacosupp  8159  mpocurryd  8219  fvmpocurryd  8221  rdgsucmptf  8367  frsucmpt  8377  oevn0  8450  oa0r  8473  om1r  8478  oe1m  8480  omass  8515  oeoalem  8532  oeoa  8533  oeoe  8535  qseq12  8708  map0g  8832  xpcomco  9005  sbthlem4  9028  sbthlem5  9029  xpmapenlem  9082  phplem2  9139  unxpdomlem3  9168  funsnfsupp  9305  ordtypelem7  9439  ttrcltr  9637  cardennn  9907  dfac9  10059  alephsing  10198  axcc3  10360  ac6num  10401  konigthlem  10491  canthp1lem2  10576  ordpipq  10865  ltrnq  10902  addclprlem2  10940  mulclprlem  10942  prlem934  10956  prlem936  10970  mulcmpblnrlem  10993  addcnsr  11058  mulcnsr  11059  axcnre  11087  recex  11782  rpnnen1lem3  12929  rpnnen1lem5  12931  xaddpnf1  13178  xaddpnf2  13179  xaddmnf1  13180  xaddmnf2  13181  rexadd  13184  xnn0xaddcl  13187  xaddnemnf  13188  xaddnepnf  13189  xadddilem  13246  addmodlteq  13908  om2uzrani  13914  om2uzrdg  13918  seqf1olem2  14004  seqf1o  14005  modexp  14200  faclbnd4lem3  14257  hashunsng  14354  hashwrdn  14509  lsw1  14529  swrdfv  14611  swrdccat  14697  ccats1pfxeqbi  14704  revfv  14725  cshwsublen  14758  wrdlen2  14906  wrdl2exs2  14908  wwlktovf1  14919  relexp0  14985  relexpcnv  14997  shftcan1  15045  remul2  15092  immul2  15099  sumss  15686  geomulcvg  15841  fprodss  15913  binomfallfaclem2  16005  bpolylem  16013  ef0lem  16043  efieq1re  16166  rpnnen2lem1  16181  ruclem3  16200  dvdsnegb  16242  dvdscmul  16251  dvds2ln  16258  dvds2add  16259  dvds2sub  16260  gcdn0val  16467  rpmulgcd  16526  lcmn0val  16564  odzval  16762  pcval  16815  pcmpt  16863  prmreclem4  16890  1arithlem2  16895  vdwlem8  16959  ramcl2lem  16980  ramtcl  16981  ramtub  16983  ramcl2  16987  ramcl  17000  setsval  17137  prfcl  18169  curf1cl  18194  curfcl  18198  hofcl  18225  yonedalem4c  18243  psssdm  18548  chneq12  18580  grplactval  19018  mulgnn0gsum  19056  cntzval  19296  f1omvdco2  19423  pmtrfinv  19436  psgnunilem5  19469  odlem2  19514  gexlem2  19557  lsmvalx  19614  efgtval  19698  efgredlema  19715  vrgpval  19742  cyggex  19873  gsumcom2  19950  fincygsubgodd  20089  dvdsrtr  20348  rnghmval  20420  abvtrivd  20809  lmhmco  21038  reslmhm  21047  lvecinv  21111  zrhmulg  21489  znzrhval  21526  ocvval  21647  mplmon2  22039  subrgasclcl  22045  coe1fv  22170  coe1fzgsumdlem  22268  evl1gsumdlem  22321  mat1dimscm  22440  dmatid  22460  scmatdmat  22480  mavmul0g  22518  1marepvmarrepid  22540  mdetunilem2  22578  gsummatr01lem3  22622  gsummatr01  22624  smadiadetlem3  22633  m2cpminvid2lem  22719  chpdmatlem2  22804  isopn3  23031  cnpval  23201  ptbasfi  23546  dfac14  23583  cnmptkk  23648  xkofvcn  23649  cnmptk1p  23650  cnmptk2  23651  xkocnv  23779  flfval  23955  ptcmplem3  24019  ptcmpg  24022  tmdmulg  24057  prdsxmslem2  24494  subgnm2  24599  nmoval  24680  fsum2cn  24838  pcovalg  24979  isclmp  25064  cphnm  25160  tcphnmval  25196  ovolctb  25457  ioorcl  25544  uniioombllem2  25550  itg1addlem3  25665  itg1climres  25681  itg2uba  25710  itg2splitlem  25715  elcpn  25901  dvexp  25920  dvexp2  25921  rolle  25957  cmvth  25958  mvth  25959  dvlip  25960  dvlipcn  25961  dvlip2  25962  dveq0  25967  dv11cn  25968  lhop1lem  25980  lhop2  25982  lhop  25983  dvcvx  25987  ftc2ditglem  26012  itgsubstlem  26015  ig1pval  26141  elply2  26161  coeid2  26204  coemul  26217  taylthlem2  26339  ulmdvlem1  26365  mtest  26369  pserval2  26376  abelthlem1  26396  abelthlem3  26398  abelthlem8  26404  abelthlem9  26405  pige3ALT  26484  0cxp  26630  leibpi  26906  igamgam  27012  mule1  27111  bposlem5  27251  lgsval3  27278  lgsdinn0  27308  dchrvmasumlem1  27458  dchrisum0flblem1  27471  rpvmasum2  27475  padicval  27580  abssid  28233  abssnid  28235  axsegconlem1  28986  ax5seglem9  29006  axpasch  29010  axeuclidlem  29031  axcontlem2  29034  finsumvtxdg2ssteplem4  29617  usgr2wlkspthlem2  29826  crctcshlem4  29888  wwlknp  29911  wlkiswwlks2lem3  29939  wwlksnred  29960  wwlksnextproplem2  29978  usgrwwlks2on  30026  umgrwwlks2on  30027  clwlkclwwlklem2a  30068  clwwisshclwwsn  30086  clwwlknlbonbgr1  30109  clwwlkn1loopb  30113  clwwlkf  30117  clwwlkext2edg  30126  wwlksext2clwwlk  30127  erclwwlknsym  30140  erclwwlkntr  30141  clwwlknon1  30167  clwwlknonex2  30179  eupth2lem3lem3  30300  eucrct2eupth  30315  fusgreghash2wspv  30405  2clwwlk2clwwlklem  30416  2clwwlk2clwwlk  30420  numclwwlk1lem2f1  30427  grpoidinvlem4  30578  grpoinvval  30594  grpodivval  30606  ipval  30774  sspgval  30800  sspsval  30802  sspnval  30808  nmooval  30834  ipasslem1  30902  ipasslem4  30905  hial0  31173  hial02  31174  ocsh  31354  pjhval  31468  hosval  31811  homval  31812  hodval  31813  hfsval  31814  hfmval  31815  braval  32015  kbval  32025  eigvalval  32031  0hmop  32054  adj0  32065  lnopeq0i  32078  nmopcoi  32166  pjclem4  32270  pj3si  32278  hstoh  32303  strlem3a  32323  hstrlem3a  32331  mdexchi  32406  atcv0eq  32450  atcv1  32451  fpwrelmap  32806  cycpmco2lem4  33190  cycpmco2lem5  33191  fxpgaval  33228  smatfval  33939  measxun2  34354  measdivcst  34368  measdivcstALTV  34369  ddeval1  34378  ddeval0  34379  ballotlemfp1  34636  signswmnd  34701  signstfvneq0  34716  signstfvc  34718  ftc2re  34742  itgexpif  34750  bnj1128  35132  subfacp1lem3  35364  subfacp1lem5  35366  cvmlift2lem3  35487  msubco  35713  altopthsn  36143  ditgeq12d  36404  fnetr  36533  fnejoin2  36551  ttcsntrsucg  36704  bj-evalid  37388  finxpreclem3  37709  finxpreclem5  37711  finxpreclem6  37712  curf  37919  curunc  37923  matunitlindf  37939  poimirlem4  37945  poimirlem25  37966  mblfinlem2  37979  mblfinlem3  37980  mbfresfi  37987  itg2addnclem  37992  itg2addnc  37995  ftc1anclem5  38018  isbnd3  38105  bndss  38107  grposnOLD  38203  ghomco  38212  xrneq12  38723  lkrval  39534  pmapval  40203  polvalN  40351  watvalN  40439  ldilset  40555  ltrnset  40564  dilsetN  40599  trnsetN  40602  trlset  40607  trlval  40608  cdleme16b  40725  cdleme31fv1  40837  cdlemg1idlemN  41018  tgrpset  41191  tendoset  41205  erngset  41246  erngplus  41249  erngmul  41252  erngset-rN  41254  erngplus-rN  41257  dvaset  41451  dvaplusg  41455  dvamulr  41458  dvavadd  41461  dvavsca  41463  diafval  41477  dvhset  41527  dvhmulr  41532  dvhvadd  41538  dvhvsca  41547  docafvalN  41568  djafvalN  41580  dibfval  41587  dicfval  41621  dihfval  41677  dihval  41678  dihvalc  41679  dihvalb  41683  dochfval  41796  djhfval  41843  lcdval  42035  mapdfval  42073  mapdn0  42115  hvmapfval  42205  hdmap1fval  42242  hdmapfval  42273  hgmapfval  42332  fmpocos  42675  sn-it0e0  42848  zaddcomlem  42908  pw2f1ocnv  43465  hbtlem7  43553  relexp0a  44143  ntrclscls00  44493  dvconstbi  44761  expgrowth  44762  addrfv  44895  subrfv  44896  mulvfv  44897  refsum2cnlem1  45468  limcperiod  46058  cncfiooiccre  46323  dvbdfbdioolem1  46356  itgioocnicc  46405  fourierdlem73  46607  fourierdlem82  46616  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  sqwvfoura  46656  etransclem46  46708  nnfoctbdjlem  46883  ovn0  46994  smflim  47205  afveu  47601  afv2eu  47686  fvmptrabdm  47741  imasetpreimafvbijlemfo  47865  lighneallem3  48070  ppivalnnprm  48088  mogoldbblem  48196  fpprel2  48217  sbgoldbwt  48253  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbnd  48285  grimco  48365  cycl3grtri  48423  lmod0rng  48705  lmodvsmdi  48855  lincdifsn  48900  lcoel0  48904  islindeps2  48959  blenn0  49049  nn0sumshdiglemA  49095  itcoval0mpt  49142  rrx2plordisom  49199  nelsubclem  49542  aacllem  50276